Revisions to Using logical equivalence to prove PL statements

Bumped by Community user

occurred May 17, 2020 at 1:03

Bumped by Community user

occurred Jan 18, 2020 at 0:03

Tweeted twitter.com/StackMma/status/1206272854247059456

occurred Dec 15, 2019 at 18:00

edited tags

Link

edited Nov 17, 2019 at 1:58

J. M.'s missing motivation ♦

125.5k
11
407
581

added 31 characters in body

Source Link

edited Nov 10, 2019 at 2:33

Ethan

225
1
9

However it can be proved with booleanLogic axioms given in documentation, with 402 steps:

booleanLogic = {ForAll[{a, b}, and[a, b] == and[b, a]],
ForAll[{a, b}, or[a, b] == or[b, a]],
ForAll[{a, b}, and[a, or[b, not[b]]] == a],
ForAll[{a, b}, or[a, and[b, not[b]]] == a],
ForAll[{a, b, c}, and[a, or[b, c]] == or[and[a, b], and[a, c]]],
ForAll[{a, b, c}, or[a, and[b, c]] == and[or[a, b], or[a, c]]]}

proof = FindEquationalProof[
  ForAll[{p, q, r}, 
   and[or[and[and[r, not[q]], not[p]], 
      and[q, not[and[q, not[or[p, r]]]]]], 
     not[and[p, not[and[q, not[r]]]]]] == 
    or[and[and[p, q], not[and[r, q]]], and[r, not[p]]]], booleanLogic]
proof["ProofGraph"]
proof["ProofNotebook"]

And here is the proof graph:

Any help would be appreciated.

However it can be proved with booleanLogic axioms given in documentation, with 402 steps:

booleanLogic = {ForAll[{a, b}, and[a, b] == and[b, a]],
ForAll[{a, b}, or[a, b] == or[b, a]],
ForAll[{a, b}, and[a, or[b, not[b]]] == a],
ForAll[{a, b}, or[a, and[b, not[b]]] == a],
ForAll[{a, b, c}, and[a, or[b, c]] == or[and[a, b], and[a, c]]],
ForAll[{a, b, c}, or[a, and[b, c]] == and[or[a, b], or[a, c]]]}

proof = FindEquationalProof[
  ForAll[{p, q, r}, 
   and[or[and[and[r, not[q]], not[p]], 
      and[q, not[and[q, not[or[p, r]]]]]], 
     not[and[p, not[and[q, not[r]]]]]] == 
    or[and[and[p, q], not[and[r, q]]], and[r, not[p]]]], booleanLogic]
proof["ProofGraph"]
proof["ProofNotebook"]

And here is the proof graph:

Any help would be appreciated.

added 31 characters in body

Source Link

edited Nov 10, 2019 at 2:11

Ethan

225
1
9

PL = {ForAll[{p, q, r}, and[p, or[p, not[p]]]True] == p], 
  ForAll[{p, q, r}, or[p, and[p, not[p]]]False] == p], 
  ForAll[{p, q, r}, or[p, or[p, not[p]]]True] == or[p, not[p]]]True], 
  ForAll[{p, q, r}, and[p, and[p, not[p]]]False] == and[p, not[p]]]False], 
  ForAll[{p, q, r}, or[p, p] == p],
  ForAll[{p, q, r}, and[p, p] == p],
  ForAll[{p, q, r}, not[not[p]] == p], 
  ForAll[{p, q, r}, or[p, q] == or[q, p]], 
  ForAll[{p, q, r}, and[p, q] == and[q, p]], 
  ForAll[{p, q, r}, or[or[p, q], r] == or[p, or[q, r]]], 
  ForAll[{p, q, r}, and[and[p, q], r] == and[p, and[q, r]]], 
  ForAll[{p, q, r}, or[p, and[q, r]] == and[or[p, q], or[p, r]]], 
  ForAll[{p, q, r}, and[p, or[q, r]] == or[and[p, q], and[p, r]]], 
  ForAll[{p, q, r}, not[and[p, q]] == or[not[p], not[q]]], 
  ForAll[{p, q, r}, not[or[p, q]] == and[not[p], not[q]]], 
  ForAll[{p, q, r}, or[p, and[p, q]] == p], 
  ForAll[{p, q, r}, and[p, or[p, q]] == p],
  ForAll[{p, q, r}, or[p, not[p]] == True],
  ForAll[{p, q, r}, and[p, not[p]] == False]}
proof = FindEquationalProof[
  ForAll[{p, q, r}, 
   not[or[and[and[pand[or[and[and[r, q]not[q]], not[p]], and[not[and[p
      and[q, q]]not[and[q, p]]]not[or[p, r]]]]]], 
     not[and[p, not[and[q, not[r]]]]]] == 
    or[not[p]or[and[and[p, q]]q], not[and[r, q]]], and[r, not[p]]]], PL]
proof["ProofGraph"]
proof["ProofNotebook"]

$$\neg(((p\land q)\land \neg p)\lor(\neg(p\land q)\land p))\equiv\neg p \lor q$$$$((r ∧ ¬q ∧ ¬p) ∨ (q ∧ ¬(q ∧ ¬(p ∨ r)))) ∧ ¬(p ∧ ¬(q ∧ ¬r))$$

$$\equiv(p ∧ q ∧ ¬(r ∧ q)) ∨ (r ∧ ¬p)$$

not[or[and[and[pand[or[and[and[r, q]not[q]], not[p]], and[not[and[p, 
 q]], p]]] == or[not[p], q]]

But seems not work, i tried shorter ones, which works fine, is it because this statement too long or something I missed $?$

Any help would be appreciated.

I added last two axioms from Logical equivalence:

ForAll[{p, q, r}, or[p, not[p]] == True],
ForAll[{pand[q, qnot[and[q, r}not[or[p, and[pr]]]]]], not[p]] == False]

Seems works now.

And $1-4$ can also changes to:

ForAll[{p, q, r}, and[p, True] == p],
ForAll[{p, q, r} not[and[p, or[pnot[and[q, False]not[r]]]]]] == p],
ForAll[{p, q, r}, or[p, True] == True],
ForAll[{p  or[and[and[p, qq], r}not[and[r, and[pq]]], False]and[r, ==not[p]]]], False]PL]

But seems not work, i tried shorter ones, which works fine, is it because this statement too long or something I missed $?$

Any help would be appreciated.

PL = {ForAll[{p, q, r}, and[p, or[p, not[p]]] == p], 
  ForAll[{p, q, r}, or[p, and[p, not[p]]] == p], 
  ForAll[{p, q, r}, or[p, or[p, not[p]]] == or[p, not[p]]], 
  ForAll[{p, q, r}, and[p, and[p, not[p]]] == and[p, not[p]]], 
  ForAll[{p, q, r}, or[p, p] == p], ForAll[{p, q, r}, and[p, p] == p],
  ForAll[{p, q, r}, not[not[p]] == p], 
  ForAll[{p, q, r}, or[p, q] == or[q, p]], 
  ForAll[{p, q, r}, and[p, q] == and[q, p]], 
  ForAll[{p, q, r}, or[or[p, q], r] == or[p, or[q, r]]], 
  ForAll[{p, q, r}, and[and[p, q], r] == and[p, and[q, r]]], 
  ForAll[{p, q, r}, or[p, and[q, r]] == and[or[p, q], or[p, r]]], 
  ForAll[{p, q, r}, and[p, or[q, r]] == or[and[p, q], and[p, r]]], 
  ForAll[{p, q, r}, not[and[p, q]] == or[not[p], not[q]]], 
  ForAll[{p, q, r}, not[or[p, q]] == and[not[p], not[q]]], 
  ForAll[{p, q, r}, or[p, and[p, q]] == p], 
  ForAll[{p, q, r}, and[p, or[p, q]] == p]}
proof = FindEquationalProof[
  ForAll[{p, q, r}, 
   not[or[and[and[p, q], not[p]], and[not[and[p, q]], p]]] == 
    or[not[p], q]], PL]
proof["ProofGraph"]
proof["ProofNotebook"]

$$\neg(((p\land q)\land \neg p)\lor(\neg(p\land q)\land p))\equiv\neg p \lor q$$

not[or[and[and[p, q], not[p]], and[not[and[p, q]], p]]] == or[not[p], q]]

But seems not work, i tried shorter ones, which works fine, is it because this statement too long or something I missed $?$

Any help would be appreciated.

I added last two axioms from Logical equivalence:

ForAll[{p, q, r}, or[p, not[p]] == True],
ForAll[{p, q, r}, and[p, not[p]] == False]

Seems works now.

And $1-4$ can also changes to:

ForAll[{p, q, r}, and[p, True] == p],
ForAll[{p, q, r}, or[p, False] == p],
ForAll[{p, q, r}, or[p, True] == True],
ForAll[{p, q, r}, and[p, False] == False]

PL = {ForAll[{p, q, r}, and[p, True] == p],
  ForAll[{p, q, r}, or[p, False] == p],
  ForAll[{p, q, r}, or[p, True] == True],
  ForAll[{p, q, r}, and[p, False] == False],
  ForAll[{p, q, r}, or[p, p] == p],
  ForAll[{p, q, r}, and[p, p] == p],
  ForAll[{p, q, r}, not[not[p]] == p],
  ForAll[{p, q, r}, or[p, q] == or[q, p]],
  ForAll[{p, q, r}, and[p, q] == and[q, p]], 
  ForAll[{p, q, r}, or[or[p, q], r] == or[p, or[q, r]]], 
  ForAll[{p, q, r}, and[and[p, q], r] == and[p, and[q, r]]], 
  ForAll[{p, q, r}, or[p, and[q, r]] == and[or[p, q], or[p, r]]], 
  ForAll[{p, q, r}, and[p, or[q, r]] == or[and[p, q], and[p, r]]], 
  ForAll[{p, q, r}, not[and[p, q]] == or[not[p], not[q]]], 
  ForAll[{p, q, r}, not[or[p, q]] == and[not[p], not[q]]], 
  ForAll[{p, q, r}, or[p, and[p, q]] == p],
  ForAll[{p, q, r}, and[p, or[p, q]] == p],
  ForAll[{p, q, r}, or[p, not[p]] == True],
  ForAll[{p, q, r}, and[p, not[p]] == False]}
proof = FindEquationalProof[
  ForAll[{p, q, r}, 
   and[or[and[and[r, not[q]], not[p]], 
      and[q, not[and[q, not[or[p, r]]]]]], 
     not[and[p, not[and[q, not[r]]]]]] == 
    or[and[and[p, q], not[and[r, q]]], and[r, not[p]]]], PL]
proof["ProofGraph"]
proof["ProofNotebook"]

$$((r ∧ ¬q ∧ ¬p) ∨ (q ∧ ¬(q ∧ ¬(p ∨ r)))) ∧ ¬(p ∧ ¬(q ∧ ¬r))$$

$$\equiv(p ∧ q ∧ ¬(r ∧ q)) ∨ (r ∧ ¬p)$$

and[or[and[and[r, not[q]], not[p]],  
          and[q, not[and[q, not[or[p, r]]]]]], 
         not[and[p, not[and[q, not[r]]]]]] == 
        or[and[and[p, q], not[and[r, q]]], and[r, not[p]]]], PL]

But seems not work, i tried shorter ones, which works fine, is it because this statement too long or something I missed $?$

Any help would be appreciated.

improved formatting

Source Link

edited Nov 9, 2019 at 22:59

Ethan

225
1
9

Loading

added 31 characters in body

Source Link

edited Nov 9, 2019 at 22:53

Ethan

225
1
9

Loading

added 31 characters in body

Source Link

edited Nov 9, 2019 at 18:59

Ethan

225
1
9

Loading

Source Link

asked Nov 9, 2019 at 6:59

Ethan

225
1
9

Loading

Stack Exchange Network

Return to Question