1
$\begingroup$

The following code will generate some ProofNotes:

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[{a, b, c}, 
   or[and[not[a], c], or[and[not[b], a], and[not[b], c]]] == 
    or[and[not[a], c], and[not[b], a]]], PL]
proof["ProofNotebook"]

This proves logic statements with logical equivalence, in this case it's proving:

or[and[not[a], c], or[and[not[b], a], and[not[b], c]]] == 
    or[and[not[a], c], and[not[b], a]]

$$(\neg a\land c)\lor((\neg b\land a)\lor(\neg b\land c))\equiv(\neg a\land c)\lor(\neg b\land a)$$

In $ \mathrm\LaTeX $ this is

(\neg a\land c)\lor((\neg b\land a)\lor(\neg b\land c))\equiv(\neg a\land c)\lor(\neg b\land a)

And here is some lines of the proof notes:

and[or[c,a],not[and[a,b]]]==or[and[not[a],c],and[not[b],a]]

$$(c\lor a)\land\neg(a\land b)\equiv(\neg a \land c) \lor (\neg b \land a)$$

In $ \mathrm\LaTeX $ this is:

(c\lor a)\land\neg(a\land b)\equiv(\neg a \land  c) \lor  (\neg b \land  a)

and[or[c,a],or[not[a],not[b]]]==or[and[not[a],c],and[not[b],a]]

$$(a \lor c) \land (\neg a \lor \neg b)\equiv (\neg a \land c) \lor (\neg b \land a)$$

In $ \rm\LaTeX $ which is:

(a \lor c) \land  (\neg a \lor  \neg b)\equiv (\neg a \land  c) \lor  (\neg b \land  a)

How do I do this conversion?

Any help would be appreciated.

$\endgroup$
4
$\begingroup$

You can use TeXForm to do most of the work for you. You only need to replace your custom operators with the built-in ones, so that TeXForm knows which symbols to use:

makeTeX[expr_] := 
 HoldForm[expr] /. {and -> And, or -> Or, not -> Not, Equal -> Congruent} // 
  TeXForm

makeTeX[and[or[c, a], not[and[a, b]]] == or[and[not[a], c], and[not[b], a]]]
(* ((c\lor a)\land \neg (a\land b))\equiv ((\neg a\land c)\lor (\neg b\land a)) *)

$((c\lor a)\land \neg (a\land b))\equiv ((\neg a\land c)\lor (\neg b\land a))$

Note the use of HoldForm to prevent the expression from evaluation when the built-in operators are substituted in.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.