Stephen M Watt <smwatt@uwaterloo.ca>
October 19, 2025
For items marked *, documentation is in progress.
LogicLab has been developed to help students who are learning logic for computing.
It provides individual functions to automate tedious or error-prone steps, allowing students to focus on higher-level planning of simplifictions and proofs. For example, it has functions to apply distributive laws on large expressions or to verify that an axiom is correctly applied in a formal proof step.
LogicLab also provides higher-level functions, for example, to
In addition, functions are provided for interctive editing to allow user-directed transformations of sub-expressions in logical formulas.
LogicLab is provided in source form as a program in the Racket programming language, a language with which all University of Waterloo computer science students use in their first year. Users can write their own higher-level programs using the set of provided functions.
This is a work in progress. There are presently the following limitations:
banana12.For advanced use, or to write extension programs, see the LogicLab Programming Reference.
For the impatient, here are pointers to some important top-level functions:
(string->lf "A → B∧C")(display-logic-truth-table-of-parts (string->lf "A → B∧C"))(lf-dnf (string->lf "(a→b) ∧ (u | v)"))(lf-arg-map (string->lf "a ∧ b ∧ ¬(c∨¬d)") 2 lf-rule-demorgan-down)(minimal-dnf (string->lf "a∧(b∨c)∧(¬a∨d)→ d"))(dpp '(p q r s) (map string->lf '("p→q" "¬q∨¬r∨s" "p∧r∧¬s")))(fd-check-proof axioms-and-theorems steps)Examples are given showing an interactive Racket session like this:
> (string->lf "A → B∧C")
'(impl A (and B C))
> (string->lf "A -> B/\\C")
'(impl A (and B C))
Here, the > characters are prompts by the Racket interface. The expression immediately following prompts, e.g. (string->lf "A→B∧C") are inputs, and the otuputs follow, e.g. '(impl A (and B C)). Note that "\" characters must be doubled to enter thenm in strings.
Sections that describe functions usually list them like this:
(example-fn ⟨string⟩ ... [⟨error-handler⟩])
The arguments given in angle brackets, "⟨ ⟩", specify their types. Optional arguments are enclosed in square brackets, "[ ]". An argument followed by an ellipsis, "...", indicates zero or more instances may be given.
LogicLab is provided as a file of functions in the Racket programming language and may be obtained from https://cs.uwaterloo.ca/~smwatt/projects/LogicLab/LogicLab.rkt .
Once you have obtained the source file, "LogicLab.rkt", you load it into Racket. One way is from the computer command line, e.g.
% racket
> (load "LogicLab.rkt")
> ;;; ... Enter your commands here ...
> (exit)
The other is from the graphical user interface DrRacket. In this case, enter the following commands in the definitions pane (the top part) and then click "Run":
#lang racket/load
(load "/Users/smwatt/Dropbox/+++ Projects/logic/LogicLab.rkt")
Logical formulas may be created either from strings or from Racket S-Expressions. Each of these has their own syntax.
(sexpr->lf ⟨s-expression⟩)
The simplest way to make a logical formula is to quote a Racket S-expression and use the sexpr->lf function.
In a quoted S-expression, the connectives are used as follow:
| Expression | Meaning |
|---|---|
| Racket identifier | propositional symbol |
#t #f |
nullary connectives ⊤ ⊥ |
(not A) |
unary connective ¬ |
(impl A B) (equiv A B) |
binary connecitves → ↔ |
(op A ...) |
n-ary connectives, n ≥ 0 |
((Q x) A) |
quantified formula (coming soon...) |
Above,
op can be any of and, or, xor, nand, nor, xnorQ can be forall or existsA, B represent S-expressions of logical sub-formulas.... means zero or more occurrences.> (sexpr->lf '(and (or a b c) (impl d (not e)) (equiv f g)))
'(and (or a b c) (impl d (not e)) (equiv f g))
> (sexpr->lf '(xor a1 a2 a3 (nand b1 b2) (or c1) (and)))
'(xor a1 a2 a3 (nand b1 b2) (or c1) (and))
(string->lf ⟨string⟩)
(parse-string ⟨string⟩ [⟨error-handler⟩])
Logical formulas may be constructed from character strings using the string->lf function. This function allows formulas to use Unicode characters for connectives or alternative syntaxes using only ASCII.
> (string->lf "A→B∧C")
'(impl A (and B C))
> (string->lf "A-> B/\\C")
'(impl A (and B C))
The functions are called using Racket syntax after the prompt >, and the results are shown as Racket data structures.
Symbols (e.g. propositional symbols) begin with an upper or lower case letter followed by letters or digits, e.g. A, n12, Banana101.
The connectives are shown below in decreasing order of precedence.
| Connective | Syntax | S-expression operation |
|---|---|---|
⊤ ⊥ |
nullary | #t #f |
∀id ∃id |
prefix | (forall id) (exists id) -- coming soon |
¬ ' |
prefix ¬, postfix ' | not |
∧ ∨ | ↓ ⊕ |
infix | and or nand nor xor |
· |
infix | and |
+ |
infix | or |
→ |
infix | impl |
↔ |
infix | equiv |
As seen above, the parse accepts both logical connectives and
boolean algebra syntax. Paretheses may be used to group subformulas as desired.
> (string->lf "A → B ∨ C")
'(impl A (or B C))
> (string->lf "(A → B) ∨ C")
'(or (impl A B) C)
The connectives ∧ ∨ | ↓ ⊕ ↔ have meaning as n-ary operations: ∧ ∨ ⊕ ↔ are associative, while | ↓ can be defined as the negation of n-ary ∧ ∨. For this reason, these are parsed to n-ary forms when one is entered consecutively at the same level. If nested forms are desired, then parentheses must be used.
The connective → is taken to be "right associative"
when used consecutvely at the same level.
> (string->lf "A ∧ B ∧ C ∧ D")
'(and A B C D)
> (string->lf "A ∧ (B ∧ C) ∧ D")
'(and A (and B C) D)
> (string->lf "A ∧ (B ∧ C ∧ D)")
'(and A (and B C D))
> (string->lf "A → B → C → D")
'(impl A (impl B (impl C D)))
Since it can be difficult to enter Unicode symbols from a keyboard, alternative syntaxes that use only ASCII characters are provided. There are alternatives that use ASCII characters to make a symbol reminiscent of the operation, and there are alternatives that use Tex-like syntax. These are shown in the table below.
| Syntax | Alternative syntax | Alternative LaTeX-like syntax |
|---|---|---|
⊤ |
#t | \top |
⊥ |
#f | \bot |
∧ · |
/\ && * |
\land |
∨ |
\/ || + |
\lor |
¬ |
prefix ! ~, postfix ' |
\lnot |
→ |
-> |
\limpl \rightarrow |
↔ |
<-> |
\lequiv \leftrightarrow \lxnor |
⊕ |
++ |
\lxor |
| |
!* | \lnand |
↓ |
!+ | \lnor \downarrow |
The symbols \tee \bot \lnot \land \lor \forall \exists as well as \rightarrow \leftrightarrow \downarrow are standard LaTeX. The symbols \limpl \lequiv \lxnor \lxor \lnand \lnor need to be defined by a LaTeX \newcommand to use them in documents.
NOTE: To enter a "\" character in a Racket string, it is necessary to double it, for example "A /\\ B" or "\\top \\land X".
> (string->lf "A && B && !(C || D)")
'(and A B (not (or C D)))
> (string->lf "A * B * (C + D)'")
'(and A B (not (or C D)))
> (string->lf "A /\\ B /\\ ~(C \\/ D)")
'(and A B (not (or C D)))
> (string->lf "A \\land B \\land \\lnot (C \\lor D)")
'(and A B (not (or C D)))
(lf->sexpr ⟨logical-formula⟩)
(lf->logic-string ⟨logical-formula⟩ [⟨error-handler⟩])
(lf->boolalg-string ⟨logical-formula⟩ [⟨error-handler⟩])
(lf->logic-latex ⟨logical-formula⟩ [⟨error-handler⟩])
(lf->boolalg-latex ⟨logical-formula⟩ [⟨error-handler⟩])
Logical formulas may be output either as Racket S-expressions or as strings. For strings, the output may be either in "logic" syntax or in "boolean algebra", and for each of these the output string mey either be in a form suitable to read in an interactive session or in LaTeX format, suitable to cut and paste into a document.
In logic syntax, connectives are shown as ⊤ ⊥ ∧ ∨ ¬ → ↔ ⊕ | ↓ and any formula can be output.
In boolean algebra syntax, only the connectives and or #t #f not may be used, and these are shown as * + 0 1 and postfix ' or overline in LaTeX.
> (define F (sexpr-lf '(and A B (not (or C D))) ))
> (lf->sexpr F)
'(and A B (not (or C D))) ))
> (lf->logic-string F)
"A∧B∧¬(C∨D)"
> (lf->boolalg-string F)
"A·B·(C+D)'"
> (lf->logic-latex F)
"A\\land B\\land \\neg \\left (C\\lor D\\right )"
> (lf->boolalg-latex F)
"A\\cdot B\\cdot \\overline{\\left (C+D\\right )}"
This section is under construction.
(truth-table-of-parts lf ⟨logical-formula⟩)
(truth-table-of-formulas ⟨list-of-symbols⟩ ⟨list-of-logical-formulas⟩)
These functions create truth tables for propositional logic. Truth tables objects are represented as a list of rows. The first is a header row, giving a list of formulas. The remaining lists are the truth values under all possible truth valuations of the given propositional symbols.
The function truth-table-of-parts takes a single logical formula and produces a truth table ranging over all truth valuations for its propositional symbols and having one column for each sub-formula.
The function truth-table-of-formulas takes a list of propositional symbols and a list of logical formulas and produces a truth table ranging over all truth valuations of the symbols and having one column for each given formula.
(truth-table->strings ⟨to-string-fn⟩ ⟨truth-table⟩)
(truth-table->latex ⟨to-latex-fn⟩ ⟨truth-table⟩)
Truth tables may be converted with the column headers in logical formula notation or boolean algebra notation, with the output as a list of Unicode strings or LaTeX. Here, to-string-fn and to-latex-fn are user-provided functions to convert individual formulas to Unicode strings or LaTeX, respectively. See the Output of Formulas for details.
(display-logic-truth-table-of-parts ⟨logical-formula⟩)
(display-boolalg-truth-table-of-parts ⟨logical-formula⟩)
(display-logic-truth-table-of-formulas ⟨list-of-symbols⟩ ⟨list-of-logical-formulas⟩)
(display-boolalg-truth-table-of-formulas ⟨list-of-symbols⟩ ⟨list-of-logical-formulas⟩)
For convenience, the display-* functions are provided to build and format truth tables in one step.
Suppose the following definitions have been made:
(define F (sexpr->lf '(and (or (not p) q) (not (or (not p) q)))))
(define Fsyms0 (list (lf-sym 'p) (lf-sym 'q)))
(define Fforms0 (list F (lf-arg F 0) (cadr Fsyms0)))
Then truth tables can be displayed in various notations, as shown in the following session:
> (display-logic-strings-truth-table-of-parts F)
p q ¬p ¬p∨q ¬(¬p∨q) (¬p∨q)∧¬(¬p∨q)
0 0 1 1 0 0
0 1 1 1 0 0
1 0 0 0 1 0
1 1 0 1 0 0
> (display-boolalg-strings-truth-table-of-parts F)
p q p' p'+q (p'+q)' (p'+q)(p'+q)'
0 0 1 1 0 0
0 1 1 1 0 0
1 0 0 0 1 0
1 1 0 1 0 0
> (display-logic-latex-truth-table-of-parts F)
\begin{tabular}{cc||cccc}
$p$ & $q$ & $\neg p$ & $\neg p\lor q$ & $\neg \left (\neg p\lor q\right )$
& $\left (\neg p\lor q\right )\land \neg \left (\neg p\lor q\right )$\\
\hline
0 & 0 & 1 & 1 & 0 & 0\\
0 & 1 & 1 & 1 & 0 & 0\\
1 & 0 & 0 & 0 & 1 & 0\\
1 & 1 & 0 & 1 & 0 & 0\\
\end{tabular}
> (display-boolalg-latex-truth-table-of-parts F)
\begin{tabular}{cc||cccc}
$p$ & $q$ & $\overline{p}$ & $\overline{p}+q$
& $\overline{\left (\overline{p}+q\right )}$
& $\left (\overline{p}+q\right ) \overline{\left (\overline{p}+q\right )}$\\
\hline
0 & 0 & 1 & 1 & 0 & 0\\
0 & 1 & 1 & 1 & 0 & 0\\
1 & 0 & 0 & 0 & 1 & 0\\
1 & 1 & 0 & 1 & 0 & 0\\
\end{tabular}
> (display-logic-strings-truth-table-of-formulas Fsyms0 Fforms0)
(¬p∨q)∧¬(¬p∨q) ¬p∨q q
0 1 0
0 1 1
0 0 0
0 1 1
Functions are provided to transform formulas using equivalence rules. Some of these apply to the top level connective, and others apply deeply to the whole expression.
It is possible to apply transformations to specific sub-formulas using the functions described in Working with Sub-Formulas.
(lf-rule-do-nothing ⟨logical-formula⟩)
(lf-rule-not-not ⟨logical-formula⟩)
(lf-rule-elim-impl ⟨logical-formula⟩)
(lf-rule-elim-equiv ⟨logical-formula⟩)
(lf-rule-elim-xor ⟨logical-formula⟩)
(lf-rule-elim-nand ⟨logical-formula⟩)
(lf-rule-elim-nor ⟨logical-formula⟩)
(lf-rule-elim-xnor ⟨logical-formula⟩)
(lf-rule-demorgan-down ⟨logical-formula⟩)
These functions apply an equivalence rule to a formula. The rule is applied to the whole formula at top level only, not recursively to subformlas. The formulas for xor, nand, nor and xnor may be n-ary.
> (lf-rule-do-nothing (sexpr->lf '(not (not a))))
'(not (not a))
> (lf-rule-not-not (sexpr->lf '(not (not a))))
'a
> (lf-rule-elim-impl (sexpr->lf '(impl a (not b))))
'(or (not a) (not b))
> (lf-rule-elim-equiv (sexpr->lf '(equiv (and a b) c)))
'(or (and (and a b) c) (and (not (and a b)) (not c)))
> (lf-rule-elim-nor (sexpr->lf '(nor u v w)))
'(not (or u v w))
> (lf-rule-elim-nand (sexpr->lf '(nand u v w)))
'(not (and u v w))
> (lf-rule-elim-xor (sexpr->lf '(xor u v w)))
'(or (and u (not (or (and v (not w)) (and (not v) w))))
(and (not u) (or (and v (not w)) (and (not v) w))))
> (lf-rule-elim-xor (sexpr->lf '(xor u)))
'u
> (lf-rule-elim-xnor (sexpr->lf '(xnor a b)))
'(not (or (and a (not b)) (and (not a) b)))
> (lf-rule-demorgan-down (sexpr->lf '(not (or a1 a2 a3))))
'(and (not a1) (not a2) (not a3))
> (lf-rule-demorgan-down (sexpr->lf '(not (and a1 a2 a3))))
'(or (not a1) (not a2) (not a3))
> (lf-rule-demorgan-down (sexpr->lf '(not (nor a1 a2 a3))))
'(nand (not a1) (not a2) (not a3))
> (lf-rule-demorgan-down (sexpr->lf '(not (nand a1 a2 a3))))
'(nor (not a1) (not a2) (not a3))
> (lf-rule-demorgan-down (sexpr->lf '(not ((exists x) A))))
'((forall x) (not A))
> (lf-rule-demorgan-down (sexpr->lf '(not ((forall x) A))))
'((exists x) (not A))
(lf-rule-assoc-left ⟨symbol⟩ ⟨logical-formula⟩)
(lf-rule-assoc-right ⟨symbol⟩ ⟨logical-formula⟩)
These functions use associativity to re-arrange formulas. In these, sym must be one of and or xor equiv.
The functions apply only to the top level sym, so if it is desired to convert all nested instances, first apply the lf-rule-assoc-nary function.
> (lf-rule-assoc-left 'or (sexpr->lf '(or a b c d e)))
'(or (or (or (or a b) c) d) e)
> (lf-rule-assoc-right 'or (sexpr->lf '(or a b c d e)))
'(or a (or b (or c (or d e))))
> (lf-rule-assoc-left 'or (sexpr->lf '(or (or a b) (or (or c d) (and e (or f g))))))
'(or (or a b) (or (or c d) (and e (or f g))))
(lf-rule-assoc-nary ⟨symbol⟩ ⟨logical-formula⟩)
(lf-not/and/or-only ⟨logical-formula⟩)
(lf-push-nots-down ⟨logical-formula⟩)
(lf-dnf ⟨logical-formula⟩)
(lf-cnf ⟨logical-formula⟩)
(lf-cnf-dnf ⟨outer-op-symbol⟩ ⟨inner-op-symbol⟩)
These functions operate on more than the top-level operator of a formula.
The lf-rule-assoc-nary function descends into nested instances of the operation given by the symbol, which must be one of the associative operators and or xor equiv.
The lf-not/and/or-only function converts a formula to use only the connectives and, or and not by applying rules to eliminate the other connectives.
The lf-push-nots-down function transforms a formula to an equivalent one where all not operations appear on atoms.
The lf-dnf and lf-cnf functions convert a formula to an equivalent one in disjunctive normal form or conjunctive normal form, respectively. These are obtained from lf-cnf-dnf as
(define lf-dnf (lf-cnf-dnf 'or 'and))
(define lf-cnf (lf-cnf-dnf 'and 'or))
> (lf-rule-assoc-nary 'or (sexpr->lf '(or (or a b) (or (or c d) (and e (or f g))))))
'(or a b c d (and e (or f g)))
> (lf-not/and/or-only (sexpr->lf '(and (impl a b) (xor u v))))
'(and (or (not a) b) (or (and u (not v)) (and (not u) v)))
> (lf-dnf (sexpr->lf '(and (impl a b) (xor u v))))
'(or (and (not a) u (not v)) (and (not a) (not u) v) (and b u (not v)) (and b (not u) v))
Unless a formula is an atom it will have a top-level connective and some number of sub-formulas. We informally call the top-level connective the "operator" and the sub-formulas the "arguments" or "children".
(lf-const? ⟨logical-formula⟩)
(lf-atom? ⟨logical-formula⟩)
(lf-not? ⟨logical-formula⟩)
(lf-and? ⟨logical-formula⟩)
(lf-or? ⟨logical-formula⟩)
(lf-impl? ⟨logical-formula⟩)
(lf-equiv? ⟨logical-formula⟩)
(lf-nand? ⟨logical-formula⟩)
(lf-nor? ⟨logical-formula⟩)
(lf-xor? ⟨logical-formula⟩)
(lf-xnor? ⟨logical-formula⟩)
(lf-forall? ⟨logical-formula⟩)
(lf-exists? ⟨logical-formula⟩)
These operations whether a logical formula is of a particular form.
(lf-arg ⟨logical-formula⟩ ⟨index⟩)
(lf-xarg ⟨logical-formula⟩ ⟨path⟩)
These operations extract sub-formulas. The lf-arg operation returns the subformula of a non-atomic formula as specified by a zero-based index.
The lf-xarg operation returns the subformula obtained by following the given path from the root operation, with each element of the list being the index of the child to follow. These are the basic functions. Several more are described in the LogicLab Programming Reference.
> (define F (sexpr->lf '(and a b (or c (not d)) (not e))))
> (lf-atom? F)
#f
> (lf-arg F 0)
'a
> (lf-atom? (lf-arg F 0))
#t
> (lf-xarg F '(2 1 0))
'd
(lf-xarg-span ⟨logical-formula⟩ ⟨path⟩ ⟨span⟩)
Sometimes it is desired to select several adjacent sub-formulas, for example to select the formulas b c d in (and a b c d e). LogicLab allows this, provided the operator is associative. To do this, the lf-xarg-span function is used.
The result is an n-ary formula combining the selected sub-formulas with the same connective as the main formula.
> (define F (sexpr->lf '(and a b (or c d e f) g)))
> (lf-xarg-span F '(2 1) 2)
'(or d e)
> (lf-xarg-span F '(2 1) 1)
'(or d)
> (lf-xarg-span F '(2 1) 0)
'(or)
> (lf-xarg-span F '(0) 2)
'(and a b)
> (lf-xarg-span F '() 1)
'(and a b (or c d e f) g)
(lf-arg-subs F n G) ; Replace arg n by G
(lf-xarg-subs F path G) ; Replace sub-formula at path by G
(lf-xarg-span-subs F path span G) ; Replace span sub-formulas with G
These functions construct a new formula where a part of a given formula is replaced.
The lf-arg-subs function replaces the n-th argument of F with G.
The lf-xarg-subs function replaces the part of F found at path with G.
The lf-xarg-span-subs function replaces the span parts of F found starting at path with G.
> (define F (sexpr->lf '(and a b (or c d e f) g)))
> (lf-arg-subs F 2 (sexpr->lf '(xor u v)))
'(and a b (xor u v) g)
> (lf-xarg-subs F '(2 1) (sexpr->lf '(xor u v)))
'(and a b (or c (xor u v) e f) g)
> (lf-xarg-subs F '() (sexpr->lf '(xor u v)))
'(xor u v)
> (lf-xarg-span-subs F '(2 1) 2 (sexpr->lf '(xor c d)))
'(and a b (or c (xor u v) f) g)
(lf-arg-map fn F n)
(lf-xarg-map fn F path)
(lf-xarg-span-map fn F path span)
If the new part to be substituted is the reslt of applying a function to the existing part, then a mapping function may be used.
> (define F (sexpr->lf '(and a b (or c d e f) g)))
> (lf-arg-map F 2 lf-not)
'(and a b (not (or c d e f)) g)
> (lf-xarg-map F '(2 1) lf-not)
'(and a b (or c (not d) e f) g)
> (lf-xarg-span-subs F '(2 1) 2 lf-not)
'(and a b (or c (not (or d e) f) g)
Functions are given to edit logical formulas by applying rules to subformulas.
The main formula is specified using the l-use! function, after which the whole formula is selected. The part that is selected is changed using the l-down, l-left, l-right and l-up operations.
The selected subformula is shown as a list of the form (>>> E <<<).
Once the desired selection is reached, it is possible to transform by a rule using the l-apply function.
If the selected part is within an associative connective, then it is possible to "grow" the selection to include neighbouring sub-expressions using g-left and g-right.
If the selected part is within an associative connective, then it is possible to move the selected part using the m-left and m-right operations.
Summary:
| Command | Effect |
|---|---|
(l-use! e) |
Set the formula to be edited |
(l-selected) |
Extract the sub-formula in focus |
(l-show) |
Display the formula being edited |
(l-apply f) |
Apply f to the sub-formula in focus |
(l-up n) |
Move the focus n levels up the parse tree |
(l-down k) |
Move focus to the k-th argument of current focus |
(l-down path) |
Move focus down path from the current focus |
(l-left n) |
Move focus to the n-th sibling to the left |
(l-right n) |
Move focus to the n-th sibling to the right |
(l-gleft n) |
Grow the focus to include n siblings to the left |
(l-gright n) |
Grow the focus to include n siblings to the right |
(l-mleft n) |
Move the sub-formula in focus n positions to the left |
(l-mright n) |
Move the sub-formula in focus n positions to the right |
Here e is a formula, f is a function, n and k are non-negative integers, and path is a list of non-negative integers.
The default value for n is 1 and for k is 0.
The following session shows how to use these functions.
> (define F (sexpr->lf
'(not (and (not (not (or a b (or (not (and x y)) e) f)))
(and u v) ))))
> (l-use! F)
(>>>> (not (and (not (not (or a b (or (not (and x y)) e) f))) (and u v))) <<<<)
> (l-down '(0 0))
(not (and (>>>> (not (not (or a b (or (not (and x y)) e) f))) <<<<) (and u v)))
> (l-apply lf-rule-not-not)
(not (and (>>>> (or a b (or (not (and x y)) e) f) <<<<) (and u v)))
> (l-down '(2 0))
(not (and (or a b (or (>>>> (not (and x y)) <<<<) e) f) (and u v)))
> (l-apply lf-rule-demorgan-down)
(not (and (or a b (or (>>>> (or (not x) (not y)) <<<<) e) f) (and u v)))
> (l-gright 1)
(not (and (or a b (or (>>>> (or (or (not x) (not y)) e) <<<<)) f) (and u v)))
> (l-up 2)
(not (and (>>>> (or a b (or (or (not x) (not y)) e) f) <<<<) (and u v)))
> (l-apply (curry lf-rule-assoc-nary 'or))
(not (and (>>>> (or a b (not x) (not y) e f) <<<<) (and u v)))
> (l-up 2)
(>>>> (not (and (or a b (not x) (not y) e f) (and u v))) <<<<)
> (l-apply lf-push-nots-down)
(>>>> (or (and (not a) (not b) x y (not e) (not f)) (or (not u) (not v))) <<<<)
> (l-apply (curry lf-rule-assoc-nary 'or))
(>>>> (or (and (not a) (not b) x y (not e) (not f)) (not u) (not v)) <<<<)
(minimal-dnf lf [dc-minterms '()])
The minimal-dnf function finds a simplest DNF form for a propositional logical formula, lf. The function accepts an optional argument, dc-minterms, which is a list of "don't care" min-terms, i.e. a list of conjunctive clauses for which the logical value of the simplified formula does not matter. If dc-minterms is not given, or is an empty list, then the resulting simplified formula is logically equivalent to lf.
> (lf->boolalg-string (minimal-dnf (string->lf "a∧(b∨c)∧(¬a∨d)→ d")))
"1"
> (define lf-original
(string->lf "a'*b*c'*d'+ a*b'*c'*d' + a*b'*c*d' + a*b'*c*d+a*b*c'*d'+a*b*c*d"))
> (define dont-cares (list (string->lf "a*b'*c'*d") (string->lf "a*b*c*d' ")))
> (define lf-simple (minimal-dnf lf1 dont-cares))
> (lf->boolalg-string lf-simple)
"a·c+b·c'·d'+a·d'"
(display-boolalg-strings-truth-table-of-formulas
'(a b c d)
(list 'a 'b 'c 'd lf-original lf-simple))
a b c d a'·b·c'·d'+a·b'·c'·d'+a·b'·c·d'+a·b'·c·d+a·b·c'·d'+a·b·c·d a·c+b·c'·d'+a·d'
0 0 0 0 0 0
0 0 0 1 0 0
0 0 1 0 0 0
0 0 1 1 0 0
0 1 0 0 1 1
0 1 0 1 0 0
0 1 1 0 0 0
0 1 1 1 0 0
1 0 0 0 1 1
1 0 0 1 0 0
1 0 1 0 1 1
1 0 1 1 1 1
1 1 0 0 1 1
1 1 0 1 0 0
1 1 1 0 0 1
1 1 1 1 1 1
Above we see lf-simple has the same truth value as lf-original, except when a*b'*c'*d is true, which is allowed by its inclusion in dont-cares.
(lf-prime-implicants lf [method prime-implicants-from-dnf])
(prime-implicants term-list)
(essential-prime-implicants pi-lset dc-minterm-lset)
(find-minimal-pi-cover pi-lset dc-minterm-lset)
(simplified-quine-mccluskey-algorithm terms)
These functions find the prime implicants for a propositional logic formula, find which are essential, and contruct a minimal set for the given logical formula.
This section is under construction.
(dpp sym-list lf-list #:verbose? [verbose? #f])
The dpp function applies the Davis-Putnam procedure to determine the consistency of a set of logical formulas. The two required arguments are a list of propositional symbols and a list of logical formulas. An optional keyword argument controls whether the function gives an explanation of what it is doing.
The dpp function converts the logical formula to conjunctive normal form and thence to a list of disjunctive clauses. The output will be either ((or)) or (). The output ((or)) is a unary and of a nullary or which is false, meaning the set of input formulas can derive false and the input formulas are inconsistent. The output () is a nullary and which is true, meaning the set of input formulas does not derive false and the input formulas are consistent.
When tracing dpp with #:verbose? #t, the clauses are displayed in set notation with the sense of propositional symbol given as +, -, or . to mean the symbol appears as a positive literal, negative literal or not at all. For example, if the propositional symbols are given as (p q r s), the clause ¬q∨¬r∨s is displayed as {.--+}.
> (dpp '(p q r s)
(map string->lf '("p→q" "¬q∨¬r∨s" "p∧r∧¬s")))
((or))
> (dpp
'(p1 p2 p3 p4 p5 p6)
(map string->lf
'("p1→p2" "¬p2" "¬p1→p3∨p4" "p3→p5" "p6→ ¬p5" "p6" "p6∨¬p6")))
()
> (dpp '(p q r s)
(map string->lf '("p→q" "¬q∨¬r∨s" "p∧r∧¬s"))
#:verbose? #t)
Formulas:
'((impl p q) (or (not q) (not r) s) (and p r (not s)))
Conjuncts:
'((or (not q) (not r) s) (or (not p) q) (or p) (or r) (or (not s)))
Clauses:
'({.--+} {-+..} {+...} {..+.} {...-})
Sym p pos: ({+...})
Sym p neg: ({-+..})
Resolving {+...} and {-+..} to get {.+..}
Eliminated p clauses: ({.--+} {..+.} {...-} {.+..})
Sym q pos: ({.+..})
Sym q neg: ({.--+})
Resolving {.+..} and {.--+} to get {..-+}
Eliminated q clauses: ({..+.} {...-} {..-+})
Sym r pos: ({..+.})
Sym r neg: ({..-+})
Resolving {..+.} and {..-+} to get {...+}
Eliminated r clauses: ({...-} {...+})
Sym s pos: ({...+})
Sym s neg: ({...-})
Resolving {...+} and {...-} to get {....}
Eliminated s clauses: ({....})
((or))
LogicLab provides functions to check formal deduction proofs. The functions operate on objects of a variety of types: entailments, rules, substitutions, justifications, steps and proofs.
An entailment corresponds to a statement of the form P1,...,Pn ⊢ C where the Ps are the "premises", each being a logical formula or a symbol representing a set of logical formulas, and C is the "conclusion" logical formula.
A rule is a template that specifies that some entailments imply others. Rules have a set of "requirements" and give a "result". They represent statements such as "If Σ ⊢ A and Σ ⊢ A → B then Σ ⊢ B".
A substitution gives replacements for symbols in logical formulas. The replacements can be logical formulas, or, if the symbol is a requirement, a set of formulas. For example, the substitution A=X, B=Y, Σ={X→Y, Y→Z, X} applied to the rule "If Σ ⊢ A and Σ ⊢ A → B then Σ ⊢ B" shows that {X→Y, Y→Z, X} ⊢ X and {X→Y, Y→Z, X} ⊢ X→Y together imply {X→Y, Y→Z, X} ⊢ Y.
A justification consists of a rule and previously proven entailments that under some substituion should match the requirements of the rule.
A step consists of an entailment, a justification and a substitution such that the substitution applied to the justification gives the result of the rule (in the justification) matching the entailment (of the step).
A proof consists of a sequence of steps.
Each of these is explained in more detail below.
(fd-ent premise-list conclusion)
(fd-ent? ob)
(fd-ent-premises ent)
(fd-ent-conclusion ent)
(string->fd-ent s)
*fd-symbols-for-sets*
A formal deduction entailment can be created using either of the fd-ent or string->fd functions.
The fd-ent function takes two arguments, the first is a list of premises and the second is a conclusion. Each of the premises is either a logical formula or a "set" of logical formulas, and the conclusion is a logical formula. A set of logical formulas may be given either by a symbol representing the set oor by a list of logical formulas with car equal to 'set.
The string->fd-ent function takes a string of the form "*premises* ⊢ *conclusion*". Here, *premises* is a comma-separated sequence of premises, where each can be a logicl formula, a symbol representing a set of logical formulas, or a sequence of comma-separated logical formulas enclosed in braces, { }.
For both fd-ent and string->fd-ent a symbol is taken to represent a set if it is in the list *fd-symbols-for-sets*, which has the initial value '(Σ Σ1 ... Σ9 Sigma Sigma1 ... Sigma9).
The functions fd-ent?, fd-ent-premises and fd-ent-conclusions, respectively, test whether a value is an entailment and return the premise list and conclusion.
> (string->fd-ent "A→B, B→C, A ⊢ A→B")
'(fd-ent ((impl A B) (impl B C) A) (impl A B))
> (string->fd-ent "Σ, A→B ⊢ A→B")
'(fd-ent (Σ (impl A B)) (impl A B))
> (string->fd-ent "A→B,{B→C, A} ⊢ A→B")
'(fd-ent ((impl A B) (set (impl B C) A)) (impl A B))
> (fd-ent (list (sexpr->lf '(impl A B))
(list 'set (sexpr->lf '(impl B C)) (sexpr->lf 'A) ))
(sexpr->lf '(impl A B)) )
'(fd-ent ((impl A B) (set (impl B C) A)) (impl A B))
(fd-rule name kind requirement-list result)
(fd-rule? ob)
(fd-rule-name rule)
(fd-rule-kind rule)
(fd-rule-requirements rule)
(fd-rule-result rule)
(mk-fd-rule name kind requirement-string-list result-string)
(mk-fd-axiom name requirement-string-list result-string)
(mk-fd-theorem name requirement-string-list result-string)
A rule is formed with a list of requirement entailments and a result entailments. If the required entailments are proved, then the rule proves the result entailment. The fd-rule function takes four arguments. The name argument can be any symbol or number, and is used to look up the rule when needed. The kind argument is for documentation purpose, and indicates the intended use of the rule either as axiom or theorem. The requirement-list is a list of required entailments and result is the resulting entailment.
The operation fd-rule? tests whether an object and the functions fd-rule-name, fd-rule-kind, fd-rule-requirements and fd-rule-result give the corresponding parts of a rule.
The operations with names mk-fd-* construct rules with the requirements and results given as strings that are parsed into requirement lists and results. The mk-fd-axiom function constructs a rule with kind being axiom and the mk-fd-theorem function constructs a rule with the kind being theorem.
> (mk-fd-axiom 'not- (list "Σ,¬A⊢B" "Σ,¬A⊢¬B") "Σ⊢A")
'(fd-rule not- axiom ((fd-ent (Σ (not A)) B) (fd-ent (Σ (not A)) (not B)))
(fd-ent (Σ) A))
> (mk-fd-axiom 'impl- (list "Σ⊢A→B" "Σ⊢A") "Σ⊢B")
'(fd-rule impl- axiom ((fd-ent (Σ) (impl A B)) (fd-ent (Σ) A)) (fd-ent (Σ) B))
> (mk-fd-theorem 'not+ (list "Σ,A⊢B" "Σ,A⊢ ¬B") "Σ⊢ ¬A")
'(fd-rule not+ theorem ((fd-ent (Σ A) B) (fd-ent (Σ A) (not B)))
(fd-ent (Σ) (not A)))
> (fd-rule 'impl- 'axiom
(list (fd-ent (list (sexpr->lf 'Σ)) (sexpr->lf '(impl A B)))
(fd-ent (list (sexpr->lf 'Σ)) (sexpr->lf 'A)) )
(fd-ent (list (sexpr->lf 'Σ)) (sexpr->lf 'B)) )
'(fd-rule impl- axiom ((fd-ent (Σ) (impl A B)) (fd-ent (Σ) A)) (fd-ent (Σ) B))
(string->fd-subs s)
(fd-inverse-subs subs)
(fd-apply-subs subs expr)
A substitution is represented as a Racket A-list, specifically a list of pairs where a pair's car is the symbol to be substituted and a pair's cdr is the replacement value.
> (string->fd-subs "A=X→Y, B=X")
((A impl X Y) (B . X))
> (string->fd-subs "A=X, Σ={X→Y,Y→Z}")
((A . X) (Σ set (impl X Y) (impl Y Z)))
Note that the element (A impl X Y), though it looks wrong, is indeed the cons cell (A . (impl X Y)).
(fd-match syn-words pattern candidate)
The function fd-match finds a substitution that matches a candidate expression to a pattern expression. In making a match, a symbol in the pattern can match any sub-formula in the candidate expression. All instances of the same symbol in the pattern must match the same sub-formula. Symbols in the list syn-words must match, e.g. if impl is in syn-words then any instance of impl in the pattern must match impl in the candidate. If the match succedes, a substitution subs is returned such that (fd-apply-subs subs pattern) is equal? to candidate. If there is no match, #f is returned.
> (fd-match '(and or) '(and A B) '(and (or A B) C))
((B . C) (A or A B))
> (fd-match '(and or) '(and (or A B) (or A C)) '(and (or X Y) (or X Z)))
((C . Z) (B . Y) (A . X))
> (fd-match '(and or) '(and A B) '(or (and A B) C))
#f
> (fd-match '(and or) '(and (or A B) '(or A C)) '(and (or X Y) (or W Z)))
#f
(fd-find-inference-match step rules prev-steps #:verbose? [verbose? #f])
The fd-find-inference-match function is used to find a substitution that supports the justification in step. The function returns the first substitution found or #f if there are none. If there is more than one match, a warning is displayed.
To find the match, the justification is retrieved from step and the proven entailments of the steps cited in the justification are retrieved. The requirements and result of the inference rule (axiom or proved theorem) cited in the justification are also retrieved. The proven entailments of the previous steps are matched against the requirements of the inference rule and the entailment of step is matched against the result of the inference rule. For these matches is not necessary that the requirements be in the same order as the cited steps or that the order of the premises be the same -- the possible permutations are tried. If there are more premises in a candidate entailment than in the requirement pattern, then they are grouped into a set as needed.
A match is a substitution for symbols in the rule-reqs and rule-result such that when
Here "exploded" means that all (set ...) instances are appended into the containing list, e.g. '((set A B) C (and D E)) becomes (A B C (and D E)).
For examples, see the section on proof checking.
(fd-just rule-name step-names)
(fd-just-rule-name just)
(fd-just-step-names just)
A justification has two parts, the name of an inference rule (axiom or proved theorem) and a list of named steps (see the section on steps) whose entailments are intended to satisfy the requirements of the inference rule.
For examples, see the section on proof checking.
(fd-step name entailment justifiction [substitution 'auto])
(mk-fd-step name entailment justification [substitution 'auto])
(fd-step? ob)
(fd-step-name rule)
(fd-step-entailment rule)
(fd-step-justification rule)
(fd-step-subs rule)
An fd-step object has four parts, its name, an entailment, a justification and a substitution. The name is used to look up the step when checking a proof that uses it; it may be a symbol or an integer. The entailment is the formal deduction result that the step claims to prove. The justification names an inference rule and previous steps to validate the entailment of the step following the application of the substitution. If the substitution is not given, then one is deduced if possible.
The fd-step and mk-fd-step functions both make step objects. The difference is that fd-step takes its arguments as entailment, justification and substitution objects while the mk-fd-step function takes them the entailment and justification as strings that are parsed to form the objects.
The fd-step?, fd-step-name, fd-step-entailment, fd-step-justification and fd-step-subs functions test whether an object is a step and retrieve a step's components.
For examples, see the section on proof checking.
(fd-proof step-list)
(mk-fd-proof step-list)
(fd-proof? ob)
(fd-proof-steps proof)
The fd-proof function constructs a proof from a list of fd-step values, and is most useful when programming.
The mk-fd-proof function constructs a proof from a list of steps in a more user friendly syntax. Each step must be given as a list as though it was an argument list to mk-fd-step. Note, if the entire list is constructed as a quoted Racket expression, then the individual parts need not be quoted.
The functions fd-proof? and fd-proof-steps test whether an object is an fd-proof and extract the list of steps, respectively.
For examples, see the section on proof checking.
LogicLab gives some pre-defined axioms and accepted theorems. Users are free to use these or not, or to add their own. The predefined rules are:
(define ax-ref (mk-fd-axiom 'Ref (list) "A⊢A" ))
(define ax-+ (mk-fd-axiom '+ (list "Σ⊢A") "Σ,B⊢A" ))
(define ax-not- (mk-fd-axiom 'not- (list "Σ,¬A⊢B" "Σ,¬A⊢¬B") "Σ⊢A" ))
(define ax-impl- (mk-fd-axiom 'impl- (list "Σ⊢A→B" "Σ⊢A") "Σ⊢B" ))
(define ax-impl+ (mk-fd-axiom 'impl+ (list "Σ,A⊢B") "Σ⊢A→B" ))
(define ax-and.L- (mk-fd-axiom 'and.L- (list "Σ⊢A∧B") "Σ⊢A" ))
(define ax-and.R- (mk-fd-axiom 'and.R- (list "Σ⊢A∧B") "Σ⊢B" ))
(define ax-and+ (mk-fd-axiom 'and+ (list "Σ⊢A" "Σ⊢B") "Σ⊢A∧B" ))
(define ax-or- (mk-fd-axiom 'or- (list "Σ,A⊢C" "Σ,B⊢C") "Σ,A∨B⊢C"))
(define ax-or.L+ (mk-fd-axiom 'or.L+ (list "Σ⊢A") "Σ⊢B∨A" ))
(define ax-or.R+ (mk-fd-axiom 'or.R+ (list "Σ⊢A") "Σ⊢A∨B" ))
(define ax-equiv.L-(mk-fd-axiom 'equiv.L- (list "Σ,A↔B⊢A" "Σ⊢B") "Σ⊢A" ))
(define ax-equiv.R-(mk-fd-axiom 'equiv.R- (list "Σ,A↔B⊢B" "Σ⊢A") "Σ⊢B" ))
(define ax-equiv+ (mk-fd-axiom 'equiv+ (list "Σ,A⊢B" "Σ,B⊢A") "Σ⊢A↔B" ))
(define th-mem (mk-fd-theorem 'mem (list) "Σ,A⊢A" ))
(define th-not+ (mk-fd-theorem 'not+ (list "Σ,A⊢B" "Σ,A⊢ ¬B") "Σ⊢ ¬A" ))
(define th-notnot- (mk-fd-theorem 'notnot- '() "¬ ¬A⊢A" ))
(define th-and.assoc (mk-fd-theorem 'and.assoc '() "(A∧B)∧C⊢A∧(B∧C)"))
(define th-or.assoc (mk-fd-theorem 'or.assoc '() "(A∨B)∨C⊢A∨(B∨C)"))
(define th-demorgan.Aup (mk-fd-theorem 'demorgan.Aup '() "¬(A∧B) ⊢ ¬A∨¬B" ))
(define th-demorgan.Oup (mk-fd-theorem 'demorgan.Oup '() "¬(A∨B) ⊢ ¬A∧¬B" ))
(define th-demorgan.Adown (mk-fd-theorem 'demorgan.Adown '() "¬A∧¬B ⊢ ¬(A∨B)" ))
(define th-demorgan.Odown (mk-fd-theorem 'demorgan.Odown '() "¬A∨¬B ⊢ ¬(A∧B)" ))
(define axioms-Lp (list
ax-ref ax-+ ax-not-
ax-impl- ax-impl+
ax-and.L- ax-and.R- ax-and+
ax-or- ax-or.L+ ax-or.R+
ax-equiv.L- ax-equiv.R- ax-equiv+))
(fd-check-step step rules prev-steps #:verbose? [verbose? #f])
(fd-check-proof rules proof #:verbose? [verbose? #f])
The fd-check-step function determines whether the entailment of the step argment is proven by application of its justification. The inference rule named in the justification is retrieved from the rules argument, which must be a list of rule objects, and the steps named in the justification are looked up in the prev-steps argument, which must be a list of step objects. If the inference rule or any of the steps cannot be found, then the check fails, returning #f. If applying the step's substitution to the justification's inference rule does not produce the entailments of the cited steps and the claim of the current step (after canonicalization), then the check fails, returning #f. Otherwise the step succeeds, returning #t.
The fd-check-proof function checks the list of steps from the given proof, in order. Each step is checked using the provided list of rules and the list of preceding checked steps. If the cheecks of all steps in the list suceed, then fd-check-proof returns #t and otherwise #f.
Consider the following proofs. The proofs Hyp-proof-subs and Hyp-proof-auto are correct, and proofs Bad-proof-subs and Bad-proof-auto are incorrect. The *-subs proofs specify the substitutions for the justifications while the *-auto proofs discover the necessary substitutions.
(define Hyp-proof-subs1 (fd-proof (list
(mk-fd-step 1 "A→B, B→C, A ⊢ A→B" '(mem) "A=A→B, Σ={B→C, A}" )
(mk-fd-step 2 "A→B, B→C, A ⊢ A" '(mem) "A=A, Σ={A→B, B→C}" )
(mk-fd-step 3 "A→B, B→C, A ⊢ B" '(impl- 1 2) "A=A, B=B, Σ={A→B, B→C, A}")
(mk-fd-step 4 "A→B, B→C, A ⊢ B→C" '(mem) "A=B→C, Σ={A→B, A}" )
(mk-fd-step 5 "A→B, B→C, A ⊢ C" '(impl- 4 3) "A=B, B=C, Σ={A→B, B→C, A}")
(mk-fd-step 6 "A→B, B→C ⊢ A→C" '(impl+ 5) "A=A, B=C, Σ={A→B, B→C}" )
)))
(define Hyp-proof-auto1 (fd-proof (list
(mk-fd-step 1 "A→B, B→C, A ⊢ A→B" '(mem))
(mk-fd-step 2 "A→B, B→C, A ⊢ A" '(mem))
(mk-fd-step 3 "A→B, B→C, A ⊢ B" '(impl- 1 2))
(mk-fd-step 4 "A→B, B→C, A ⊢ B→C" '(mem))
(mk-fd-step 5 "A→B, B→C, A ⊢ C" '(impl- 4 3))
(mk-fd-step 6 "A→B, B→C ⊢ A→C" '(impl+ 5))
)))
(define Hyp-proof-subs2 (mk-fd-proof '(
[1 "A→B, B→C, A ⊢ A→B" (mem) "A=A→B, Σ={B→C, A}" ]
[2 "A→B, B→C, A ⊢ A" (mem) "A=A, Σ={A→B, B→C}" ]
[3 "A→B, B→C, A ⊢ B" (impl- 1 2) "A=A, B=B, Σ={A→B, B→C, A}"]
[4 "A→B, B→C, A ⊢ B→C" (mem) "A=B→C, Σ={A→B, A}" ]
[5 "A→B, B→C, A ⊢ C" (impl- 4 3) "A=B, B=C, Σ={A→B, B→C, A}"]
[6 "A→B, B→C ⊢ A→C" (impl+ 5) "A=A, B=C, Σ={A→B, B→C}" ]
)))
(define Hyp-proof-auto2 (mk-fd-proof '(
[1 "A→B, B→C, A ⊢ A→B" (mem) ]
[2 "A→B, B→C, A ⊢ A" (mem) ]
[3 "A→B, B→C, A ⊢ B" (impl- 1 2)]
[4 "A→B, B→C, A ⊢ B→C" (mem) ]
[5 "A→B, B→C, A ⊢ C" (impl- 4 3)]
[6 "A→B, B→C ⊢ A→C" (impl+ 5) ]
)))
(define Bad-proof-subs (mk-fd-proof '(
[S1 "A→B, B→C, A ⊢ A→B" (mem) "A=A→B, Σ={B→C, A}" ]
[S2 "A→B, B→C, A ⊢ B" (mem) "A=A, Σ={A→B,B→C}" ]
[S3 "A→B, B→C, A ⊢ B" (impl- S1 S2) "A=A, B=B, Σ={A→B,B→C,A}"]
[S4 "A→B, B→C, A ⊢ B→C" (mem) "A=B→C, Σ={A→B,A}" ]
[S5 "A→B, B→C, A ⊢ C" (impl- S4 S3) "A=B, B=C, Σ={A→B,B→C,A}"]
[S6 "A→B, B→C ⊢ A→C" (impl+ S5) "A=A, B=C, Σ={A→B,B→C}" ]
)))
(define Bad-proof-auto (mk-fd-proof '(
[S1 "A→B, B→C, A ⊢ A→B" (mem) ]
[S2 "A→B, B→C, A ⊢ B" (mem) ]
[S3 "A→B, B→C, A ⊢ B" (impl- S1 S2)]
[S4 "A→B, B→C, A ⊢ B→C" (mem) ]
[S5 "A→B, B→C, A ⊢ C" (impl- S4 S3)]
[S6 "A→B, B→C ⊢ A→C" (impl+ S5) ]
)))
(define (test-proof-and-report name proof expected)
(printf "Checking ~a ========~n" name)
(let ([result (fd-check-proof (cons th-mem axioms-Lp) proof #:verbose? #t)])
(if (equal? result expected)
(printf "As expected!~n")
(printf "***** Not Expected *****~n"))))
(test-proof-and-report "Checking Hyp-proof-subs1" Hyp-proof-subs1 #t)
(test-proof-and-report "Checking Hyp-proof-auto1" Hyp-proof-auto1 #t)
(test-proof-and-report "Checking Hyp-proof-subs2" Hyp-proof-subs2 #t)
(test-proof-and-report "Checking Hyp-proof-auto2" Hyp-proof-auto2 #t)
(test-proof-and-report "Checking Bad-proof-subs" Bad-proof-subs #f)
(test-proof-and-report "Checking Bad-proof-auto" Bad-proof-auto #f)
This gives the following output:
Checking Checking Hyp-proof-subs1 ========
Checking step 1: Subst given. OK
Checking step 2: Subst given. OK
Checking step 3: Subst given. OK
Checking step 4: Subst given. OK
Checking step 5: Subst given. OK
Checking step 6: Subst given. OK
Proof OK!
As expected!
Checking Checking Hyp-proof-auto1 ========
Checking step 1: Subst found A = A→B, Σ = {B→C, A}. OK
Checking step 2: Subst found A = A, Σ = {A→B, B→C}. OK
Checking step 3: Subst found A = A, B = B, Σ = {A→B, B→C, A}. OK
Checking step 4: Subst found A = B→C, Σ = {A→B, A}. OK
Checking step 5: Subst found A = B, B = C, Σ = {A→B, B→C, A}. OK
Checking step 6: Subst found B = C, A = A, Σ = {A→B, B→C}. OK
Proof OK!
As expected!
Checking Checking Hyp-proof-subs1 ========
Checking step 1: Subst given. OK
Checking step 2: Subst given. OK
Checking step 3: Subst given. OK
Checking step 4: Subst given. OK
Checking step 5: Subst given. OK
Checking step 6: Subst given. OK
Proof OK!
As expected!
Checking Checking Hyp-proof-auto1 ========
Checking step 1: Subst found A = A→B, Σ = {B→C, A}. OK
Checking step 2: Subst found A = A, Σ = {A→B, B→C}. OK
Checking step 3: Subst found A = A, B = B, Σ = {A→B, B→C, A}. OK
Checking step 4: Subst found A = B→C, Σ = {A→B, A}. OK
Checking step 5: Subst found A = B, B = C, Σ = {A→B, B→C, A}. OK
Checking step 6: Subst found B = C, A = A, Σ = {A→B, B→C}. OK
Proof OK!
As expected!
Checking Checking Bad-proof-subs ========
Checking step S1: Subst given. OK
Checking step S2: Subst given. Failed
Proof fails at step S2.
Proof failed.
As expected!
Checking Checking Bad-proof-auto ========
Checking step S1: Subst found A = A→B, Σ = {B→C, A}. OK
Checking step S2: No substitution works. Failed
Proof fails at step S2.
Proof failed.
As expected!