lbhelper

Overview ¶

Lbhelper is a program primarily designed for help with producing the logic textbook at https://github.com/adamay909/logicbook but it can do some other things, too. It can:

• convert formulas in Polish notation to a LaTeX code for a more standard infix notation;
• convert formulas in Polish to a more standard infix notation in Unicode;
• convert formulas in Polish to a more standard infix notation in ASCII;
• convert formulas in infix notation to Polish notation;
• generate truth tables for a given formula;
• generate LaTeX code for syntax trees of a formula;
• generate LaTeX code for a tree representation of a semantic tableau of a formula;
• compile a LaTeX fragment to PDF.

**The LaTeX markup generated by lbhelper requires the use of custom commands defined in the style files included with the source files for the logic textbook.**

The following symbols are used for the Polish notation (also see examples below):

negation: N
conjunction: K
disjunction: A
conditional: C
universal quantifier: U
existential quantifier: X

For input in infix notation, we use the following ASCII characters for the logical constants:

negation: -
conjunction: ^
disjunction: v
material implication: >
universal quantifier: U
existential quantifier: X

This facilitates typing.

Examples ¶

Convert formula to LaTeX code (this is the default behavior with no flags provided):

$ lbhelper CKCpqNqNp
\p{\big[\big(p\limplies q\big)\land \lnot  q\big]\mc{\limplies }\lnot  p}

Convert formula to infix in Unicode:

$ lbhelper -txt CKCpqNqNp
[(p⊃q)∧¬q]⊃¬p

Lbhelper also handles the language of first-order logic by supplying the flag -p:

$ lbhelper -p -txt CUxFxFa
∀xFx⊃Fa

Convert formula to infix in ASCII:

$ lbhelper -ascii CKCpqNqNp
((p>q)^-q)>-p

The ASCII version is ugly but can be typed. You can convert formula from ASCII infix to Polish:

$ lbhelper -infix -polish '((p>q)^-q)>-p'
CKCpqNqNp

$ lbhelper -infix -p -polish 'UxFx > -Xx-Fx'
CUxFxNXxNFx

Convert formula from ASCII infix to LaTeX:

$ lbhelper -p -infix 'XxGx > -UxGx'
\p{\lthereis x  Gx\mc{\limplies }\lnot  \lforall x  Gx}

The identity sign can also be used. For the Polish notation, the identity sign gets treated as a 2-place predicate. In the infix notation, it is used in the normal fashion. For the infix notation, you can use /= to stand for 'not equal':

$ lbhelper -p -ascii UxXyN=xy
UxXyx/=y

$ lbhelper -p -txt UxXyN=xy
∀x∃yx≠y

$ lbhelper -infix -p -polish 'a=b > (Fa>Fg)'
C=abCFaFg

LaTeX output will produce an appropriate LaTeX markup as well.

Produce truth table in Unicode:

	$lbhelper -tt -txt CKCpqNqNp
 	 p  q  |  p⊃q  ¬q  (p⊃q)∧¬q  ¬p  [(p⊃q)∧¬q]⊃¬p
	-------+---------------------------------------
	 T  T  |   T   F      F      F         T
	 F  T  |   T   F      F      T         T
	 T  F  |   F   T      F      F         T
	 F  F  |   T   T      T      T         T

Produce truth table in a narrower format that's common in textbooks (if that's your sort of thing):

$ lbhelper -ttn -txt CKCpqNqNp
 p  q  |  [(p  ⊃  q)  ∧  ¬  q]  |⊃|  ¬  p
-------+----------------------------------
 T  T  |   T   T  T   F  F  T   |T|  F  T
 F  T  |   F   T  T   F  F  T   |T|  T  F
 T  F  |   T   F  F   F  T  F   |T|  F  T
 F  F  |   F   T  F   T  T  F   |T|  T  F

You can, of course, generate LaTeX code for a truth table as well:

$ lbhelper -tt CKCpqNqNp
%truth table of:
% CKCpqNqNp
%generated by gentzen
\begin{tabular}{cc|c|c|c|c||c}
\p{p} & \p{q} & \p{p\mc{\limplies }q} & \p{\mc{\lnot } q} & \p{\big(p\limplies q\big)\mc{\land }\lnot  q} & \p{\mc{\lnot } p} & \p{\big[\big(p\limplies q\big)\land \lnot  q\big]\mc{\limplies }\lnot  p}\\
\hline
\emph{T} & \emph{T} & \emph{T} & \emph{F} & \emph{F} & \emph{F} & \emph{T}\\
\emph{F} & \emph{T} & \emph{T} & \emph{F} & \emph{F} & \emph{T} & \emph{T}\\
\emph{T} & \emph{F} & \emph{F} & \emph{T} & \emph{F} & \emph{F} & \emph{T}\\
\emph{F} & \emph{F} & \emph{T} & \emph{T} & \emph{T} & \emph{T} & \emph{T}\\
\end{tabular}

This is mostly for kicks but lbhelper can also produce an outline of a proof in the sequent calculus style used in the textbook:

$ lbhelper -proof -txt CKCpqNqNp
1. ¬q ⊢ ¬q...Assumption
2. q ⊢ q...Assumption
3. ¬p ⊢ ¬p...Assumption
4. q, p, ¬q ⊢ ¬p...1,2
5. p, ¬q, ¬p ⊢ ¬p...3
6. p, ¬q, ¬p∨q ⊢ ¬p...4,5
7. p, ¬q, p⊃q ⊢ ¬p...6
8. p, (p⊃q)∧¬q ⊢ ¬p...7
9. p ⊢ p...Assumption
10. p, ¬¬[(p⊃q)∧¬q] ⊢ ¬p...8
11. p, ¬¬[(p⊃q)∧¬q] ⊢ p...9
12. ¬¬p, ¬¬[(p⊃q)∧¬q] ⊢ ¬p...10
13. ¬¬p, ¬¬[(p⊃q)∧¬q] ⊢ p...11
14. ¬¬[(p⊃q)∧¬q]∧¬¬p ⊢ ¬p...12
15. ¬¬[(p⊃q)∧¬q]∧¬¬p ⊢ p...13
16.  ⊢ ¬{¬¬[(p⊃q)∧¬q]∧¬¬p}...14,15
17.  ⊢ ¬[(p⊃q)∧¬q]∨¬p...16
18.  ⊢ [(p⊃q)∧¬q]⊃¬p...17

It's not a full proof as there are many gaps. But the textbook and the exercises show how concretely to fill most of the gaps and the remaining ones can be figured out quickly. These automatically generated proofs mostly lack elegance and insight but they work.

You can also generate LaTeX code for semantic tableaux. Like proof outlines above, the semantic tableaux are auto-generated but they work:

$ lbhelper -tableau -infix '((p>q)^-p)>-q'
\begin{forest}
%semantic tableau of:
% CKCpqNpNq
%generated by gentzen
[ \p{\big[\big(p\limplies q\big)\land \lnot  p\big]\mc{\limplies }\lnot  q}
[ \p{\mc{\lnot } \big[\big(p\limplies q\big)\land \lnot  p\big]}
[ \p{\mc{\lnot } \big(p\limplies q\big)}
[ \p{p}
[ \p{\mc{\lnot } q}
 ]
 ]
 ]
[ \p{\mc{\lnot } \lnot  p}
[ \p{p}
 ]
 ]
 ]
[ \p{\mc{\lnot } q}
 ]
 ]
\end{forest}

Input/Output ¶

By default lbhelper outputs to Stdout. If, and only if, Stdout is detected to be a terminal, the output is followed by a newline. This helps with piping the output to other program (like a LaTeX compiler) where a newline may not be desired.

You can direct the output to a file with the -dest flag:

$lbhelper -dest table.tex -tt CKCpqNqNp

outputs the result to table.tex.

If, and only if, there is no non-flag argument, the input is taken to be Stdin. If Stdin is detected to be a terminal, you get a very primitive interactive interface:

$ lbhelper -txt
Enter formula: Cpq
p⊃q
Enter formula: Kpq
p∧q
Enter formula: Np
¬p
Enter formula:

It will continue until you enter an empty line (or send EOF or terminate it in some other way like Ctrl-C).

You can't directly specify a file as input but you can pipe the output from another program to lbhelper to achieve the same. E.g.:

$ cat list | lbhelper -tt -dest tables.tex

will take the lines of list, produce truth tables for each line, and save the results to tables.tex.

Compiling LaTeX fragments ¶

When you save the LaTeX output to file using the -dest flag, you get a LaTeX fragment that cannot be compiled as is. You can use lbhelper to compile the fragment without having to edit the fragment manually. For instance given the fragment tables.tex from above, you can compile it using:

lbhelper -compile tables.tex

The output file name is tables.pdf (as you would except from normal LaTeX compilation).

For this to work, you need:

• latexmk
• use a unicode aware LaTeX compiler (I use XeLaTeX but LuaLaTeX will probably work, too)
• the style files included with the source files of the textbook installed somewhere the LaTeX compiler can find or in the same directory as the source file.

The needed style files also include commands to facilitate the creation of exercises so you can generate the exercises proper as well as the answer keys from the same LaTeX fragment. See the source files exercises included with the textbook for some examples. You can compile answer keys using:

lbhelper -compile -answer filename.tex

The output file name gets the suffix _answers; e.g., filename_answers.pdf.

Given the -compile flag, all flags other than -answer are ignored.

NOTE: Many of the source files for the exercises for the textbook require enabling LaTeX to run lbhelper as an external command during compilation.

List of all flags ¶

-answer
  	compile with answers
-ascii
  	output formatted as you would type into proofchecker
-c	use conditional (default true)
-compile
  	compile latex fragment
-dest string
  	write output to named file (defaults to stdout)
-e	print formula as English (for LaTeX)
-f	print Latex of string (deprecated. use -l instead
-fontsize string
  	fontsize in pt (default "10pt")
-infix
  	input is in infix notation (formula typed as in the proofchecker UI
-l	output formatted in Latex (default) (default true)
-letterpaper
  	use letter size paper for compile
-m	enclose output in math mode (default true)
-normalize
  	normalize output string
-p	turn on predicate logic processing
-polish
  	print Polish notation of string
-pretty
  	prettify brackets (default true)
-proof
  	print outline of proof
-resize
  	resize to fit page
-s	interpret input as a sequent (deprecated. use -seq instead
-seq
  	interpret input as a sequent; turnstile represented by colon
-standalone
  	make fragment into a standalone LaTeX document
-stf
  	print full syntax tree
-sts
  	print simple syntax tree
-tableau
  	print semantic tableaux (output is LaTeX code)
-tt
  	print truth table
-ttn
  	print narrow truth table
-txt
  	output formatted as infix with unicode logical symbols