# Convert ProofNotes to $\mathrm\LaTeX$ logic expression

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.

## 1 Answer

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.