Demo: Propositional Proving

(Double-click on the vertical bars in order to open/close the sections)

Starting the System

The following command will load the Theorema system. (Click on the command and press ⟨Shift⟩⟨Enter⟩ in order to execute it.)

<< Theorema`

The following command sets the PropositionalProver as the default prover to be used in the command Prove.

SetGlobals[Prover -> PropositionalProver]

Each of the following commands controls the appearance of the labels in the generated proofs.

SetGlobals[LabelStyle -> "Alphanumeric"]

SetGlobals[LabelStyle -> "Numeric"]

Using the Prover and its Options

Using the Prover

By using the palette FormalTextLanguage (menu File/Palettes), you can define new propositions as follows:

Proposition["conclusion",
	({{(A ∧ B ∧ C)⟺A, "abc"}})]

Proposition["assumptions",
	({{A⟹B, "ab"}, {C, "c"}})]

(The logical connectives can be typed using the palette CompleteCharacters/Operators or using the Escape key: ⟨ESC⟩not⟨ESC⟩, ⟨ESC⟩and⟨ESC⟩, ⟨ESC⟩or⟨ESC⟩, ⟨ESC⟩==>⟨ESC⟩, ⟨ESC⟩<==>⟨ESC⟩.)

The following command generates the proof:

Prove[Proposition["conclusion"], 
      using -> Proposition["assumptions"], 
      by -> PropositionalProver]

(The arrow "->" can be  typed as ⟨ESC⟩->⟨ESC⟩.)

The proof is presented in a separate notebook and the structure of the proof is represented by the nesting of the cells indicated by the vertical bars on the right-hand side. By double-click on such a bar you can open/close the respective group of cells. Select the topmost cell by single-click on the rightmost vertical bar, then press ⟨Alt⟩ } (on Windows ⟨Ctrl⟩ }) in order to close all  the subcells, then open various groups of cells for studying the proof at the desired level of detail.

If the following command has already been executed in this session:

SetGlobals[Prover -> PropositionalProver]

then the prover does not have to be specified in the Prove command:

Prove[Proposition["conclusion"], 
      using -> Proposition["assumptions"]]

The option "using-> …" may also be missing if no assumptions are needed for the proof:

Proposition["independent",
	({{((A⟹B) ∧ 
                    C)⟹((A ∧ B ∧ 
                        C)⟺A), "abc"}})]

Prove[Proposition["independent"]]

Options of the Propositional Prover

The behavior of the propositional prover can be controlled by options, which are listed by the  command:

Options[PropositionalProver]

The meaning of the options can be found out by commands like:

?BackChaining

?TrySubgoalImplication

All the options are set to False by default. Setting such an option to True will  create  several proof alternatives: some of them may fail, but when they succeed they may lead to more natural proofs. Example:

Proposition["disjunction",
	({{(P ∧ 
                    Q ∧ (P ∧ Q)⟹
                      R)⟹(A ∨ R ∨ B), "p"}})]

Prove[Proposition["disjunction"]]

Prove[Proposition["disjunction"], 
      ProverOptions -> {TryAlternatives -> True, 
          BackChaining -> True}]

The proof generated by the previous command has failed branches and pending branches. One can display only the successful branches using the options for the simplification of proofs - see below.

Options for the Simplification of Proofs

The proof presented in the previous paragraph contains branches which are not necessary for the success. The following command results in a proof whithout unnecessary branches.

Proposition["disjunction",
	({{(P ∧ 
                    Q ∧ (P ∧ Q)⟹
                      R)⟹(A ∨ R ∨ B), "p"}})]

Prove[Proposition["disjunction"], 
      transformBy -> ProofSimplifier, 
      TransformerOptions -> {branches -> Proved}, 
      ProverOptions -> {TryAlternatives -> True, 
          BackChaining -> True}]

The option transformBy indicates which operation is performed on the resulting proof-object.

?transformBy

Options[Prove]

Setting transformBy->ProofSimplifier  results in simplifying the proof-object before display.

The option transformBy indicates which operation is done on the resulting proof-object. Furthermore the option TransformerOptions of the command Prove will be passed to  ProofSimplifier.

Options[ProofSimplifier]

For instance, branches controls the number of branches which are displayed.

?branches

?steps

In order to simplify proofs by all available methods use:

SetOptions[Prove, transformBy -> ProofSimplifier, 
      TransformerOptions -> {steps -> Essential}]

In fact one does not need to repeat the Prove command in order to see varios versions of the simplified proof. After a Prove is executed, the proof-object is returned as the result of the command, and also stored in the global variable $TmaProofObject. The proof-object can be shown as proof-notebook using ProofShow and can be simplified using ProofSimplifier.

$TmaProofObject

ProofShow[$TmaProofObject]

ProofSimplifier[$TmaProofObject, steps -> Essential]

ProofShow[%]

Other Options for Proving: Search Depth

The behavior of any prover in Theorema can be controlled by additional options, which are listed by the  command:

Options[Prove]

Of particular interest is the option SearchDepth.

Proposition["assoc left",
	({{((AB ∧ ¬ C) ∨ ((¬ AB) ∧ 
                        C))⟹((A ∧ ¬ BC) ∨ ((¬ A) ∧ BC)), "abc"}})]

Proposition["assoc right",
	({{((AB ∧ ¬ C) ∨ ((¬ AB) ∧ 
                        C))⟸((A ∧ ¬ BC) ∨ ((¬ A) ∧ BC)), "abc"}})]

Proposition["asm",
	({{AB⟺((A ∧ ¬ B) ∨ ((¬ A) ∧ B)), "ab"}, {BC⟺((B ∧ ¬ C) ∨ ((¬ B) ∧ C)), "bc"}})]

Timing[Prove[Proposition["assoc left"], 
        using -> Proposition["asm"], SearchDepth -> 50]]

Timing[Prove[Proposition["assoc right"], 
        using -> Proposition["asm"], SearchDepth -> 50]]

When you are out of patience with a long proof and you use the menu Kernel/AbortEvaluation, then you can still see the part of the proof which was produced using:

ProofShow[$TmaProofObject]

Propositions Involving Truth Constants

Truth Constants As Goals and As Assumptions

Definitions which are Necessary for the Other Subsections

Proposition["True",
	({{True, "t"}})]

Proposition["False",
	({{False, "f"}})]

Proposition["Negated True",
	({{¬ True, "nt"}})]

Proposition["Negated False",
	({{¬ False, "nf"}})]

Proposition["Any",
	({{X, "x"}})]

Truth Constants as Goals without Assumptions

Prove[Proposition["True"]]

Prove[Proposition["False"]]

Prove[Proposition["Negated True"]]

Prove[Proposition["Negated False"]]

Truth Constants as Goals with Arbitrary Assumptions

Prove[Proposition["True"], 
      using -> Proposition["Any"]]

Prove[Proposition["False"], 
      using -> Proposition["Any"]]

Prove[Proposition["Negated True"], 
      using -> Proposition["Any"]]

Prove[Proposition["Negated False"], 
      using -> Proposition["Any"]]

Truth Constants as Assumptions with Arbitrary Goals

Prove[Proposition["Any"], 
      using -> Proposition["True"]]

Prove[Proposition["Any"], 
      using -> Proposition["False"]]

Prove[Proposition["Any"], 
      using -> Proposition["Negated True"]]

Prove[Proposition["Any"], 
      using -> Proposition["Negated False"]]

Truth Constants as Assumptions and Goals

Prove[Proposition["True"], 
      using -> Proposition["False"]]

Prove[Proposition["True"], 
      using -> Proposition["Negated True"]]

Prove[Proposition["True"], 
      using -> Proposition["Negated False"]]

Prove[Proposition["False"], 
      using -> Proposition["True"]]

Prove[Proposition["False"], 
      using -> Proposition["Negated True"]]

Prove[Proposition["False"], 
      using -> Proposition["Negated False"]]

Prove[Proposition["Negated True"], 
      using -> Proposition["True"]]

Prove[Proposition["Negated True"], 
      using -> Proposition["False"]]

Prove[Proposition["Negated True"], 
      using -> Proposition["Negated False"]]

Prove[Proposition["Negated False"], 
      using -> Proposition["True"]]

Prove[Proposition["Negated False"], 
      using -> Proposition["False"]]

Prove[Proposition["Negated False"], 
      using -> Proposition["Negated True"]]

Simplification of Formulae Containing Truth Constants

Negation

Proposition["Negated True",
	({{(¬ True)⟺False, "nt"}})]

Prove[Proposition["Negated True"]]

Proposition["Negated False",
	({{(¬ False)⟺True, "nf"}})]

Prove[Proposition["Negated False"]]

Conjunction

Proposition["True Conjunct",
	({{(A ∧ True)⟺A, "tc"}})]

Proposition["True Conjunct",
	({{(A ∧ ¬ False)⟺A, "tc"}})]

Prove[Proposition["True Conjunct"]]

Proposition["False Conjunct",
	({{(A ∧ False)⟺False, "fc"}})]

Proposition["False Conjunct",
	({{(A ∧ ¬ True)⟺False, "fc"}})]

Prove[Proposition["False Conjunct"]]

Disjunction

Proposition["True Alternative",
	({{(A ∨ True)⟺True, "ta"}})]

Proposition["True Alternative",
	({{(A ∨ ¬ False)⟺True, "ta"}})]

Prove[Proposition["True Alternative"]]

Proposition["False Alternative",
	({{(A ∨ False)⟺A, "fa"}})]

Proposition["False Alternative",
	({{(A ∨ ¬ True)⟺A, "fa"}})]

Prove[Proposition["False Alternative"], 
      ProverOptions -> {BackChaining -> True}]

Proposition["test",
	({{((A ∨ ¬ True) ∧ (A⟹
                        B))⟹B, "fa"}})]

Prove[Proposition["test"], 
      ProverOptions -> {BackChaining -> True}]

Implication

Proposition["True Implicand",
	({{(True⟹A)⟺
                A, "tid"}})]

Prove[Proposition["True Implicand"], 
      ProverOptions -> {BackChaining -> True}]

Proposition["False Implicand",
	({{(False⟹A)⟺
                True, "fid"}})]

Prove[Proposition["False Implicand"]]

Proposition["True Implicatum",
	({{(A⟹True)⟺
                True, "tim"}})]

Prove[Proposition["True Implicatum"]]

Proposition["False Implicatum",
	({{(A⟹
                    False)⟺¬ A, "fim"}})]

Prove[Proposition["False Implicatum"], 
      ProverOptions -> {BackChaining -> True}]

Equivalence

Proposition["True Left Side",
	({{(True⟺
                    A)⟺A, "tls"}})]

Prove[Proposition["True Left Side"], 
      ProverOptions -> {BackChaining -> True}]

Proposition["True Right Side",
	({{(True⟺
                    A)⟺A, "trs"}})]

Prove[Proposition["True Right Side"], 
      ProverOptions -> {BackChaining -> True}]

Proposition["False Left Side",
	({{(False⟺
                    A)⟺¬ A, "fls"}})]

Prove[Proposition["False Left Side"], 
      ProverOptions -> {BackChaining -> True}]

Proposition["False Right Side",
	({{(False⟺
                    A)⟺¬ A, "frs"}})]

Prove[Proposition["False Right Side"], 
      ProverOptions -> {BackChaining -> True}]

Propositional Logic is Boolean Algebra

Proposition["Tertium non datur",
	({{A ∨ (¬ A), "tnd"}})]

Prove[Proposition["Tertium non datur"]]

Proposition["No contradiction",
	({{¬ (A ∧ (¬ A)), "nc"}})]

Prove[Proposition["No contradiction"]]

Proposition["True alternative",
	({{A ∨ True, "ta"}})]

Prove[Proposition["True alternative"]]

Proposition["True conjunctive fails",
	({{A ∧ True, "tcf"}})]

Prove[Proposition["True conjunctive fails"]]

Proposition["True conjunctive",
	({{(A ∧ True)⟺A, "tc"}})]

Prove[Proposition["True conjunctive"]]

Proposition["False conjunctive",
	({{(A ∧ False)⟺False, "fc"}})]

Prove[Proposition["False conjunctive"]]

Proposition["False alternative fails",
	({{A ∨ False, "fcf"}})]

Prove[Proposition["False alternative fails"]]

Proposition["False alternative",
	({{(A ∨ False)⟺A, "fa"}})]

Prove[Proposition["False alternative"]]

Prove[Proposition["False alternative"], 
      ProverOptions -> {BackChaining -> True}]

Proposition["Commutativity of ∧",
	({{(A ∧ B)⟺(B ∧ A), "ca"}})]

Prove[Proposition["Commutativity of ∧"]]

Proposition["Commutativity of ∨",
	({{(A ∨ B)⟺(B ∨ A), "co"}})]

Prove[Proposition["Commutativity of ∨"]]

Proposition["Idempotency of ∧",
	({{(A ∧ A)⟺A, "ia"}})]

Prove[Proposition["Idempotency of ∧"]]

Proposition["Idempotency of ∨",
	({{(A ∨ A)⟺A, "io"}})]

Prove[Proposition["Idempotency of ∨"]]

Proposition["Associativity of ∧",
	({{(( A  ∧  B)  ∧  
                    C)⟺ ( 
                  A  ∧  (B  ∧  C)), "aa"}})]

Prove[Proposition["Associativity of ∧"]]

Proposition["Associativity of ∨",
	({{(( A  ∨  B)  ∨  
                    C)⟺ ( 
                  A  ∨  (B  ∨  C)), "ao"}})]

Prove[Proposition["Associativity of ∨"]]

Proposition["Distributivity of ∨",
	({{(( A  ∧  B)  ∨  
                    C)⟺ (( 
                      A ∨  C) ∧  (B  ∨  C)), "do"}})]

Prove[Proposition["Distributivity of ∨"]]

Proposition["Distributivity of ∧",
	({{(( A  ∨  B)  ∧  
                    C)⟺ (( 
                      A ∧  C) ∨  (B  ∧  C)), "da"}})]

Prove[Proposition["Distributivity of ∧"]]

Proposition["Absorption of ∧ over ∨",
	({{(( A  ∧  B)  ∨  
                    A) ⇔  A, "aao"}})]

Prove[Proposition["Absorption of ∧ over ∨"]]

Proposition["Absorption of ∨ over ∧",
	({{(( A  ∨  B)  ∧  
                    A) ⇔  A, "aoa"}})]

Prove[Proposition["Absorption of ∨ over ∧"]]

Proposition["Double Negation",
	({{(¬ ¬ A)⟺A, "dn"}})]

Prove[Proposition["Double Negation"]]

Proposition["De Morgan for ∧",
	({{(¬  (A  ∧  
                        B) ) ⇔  ( (¬ A) ∨ (¬ B)), "ma"}})]

Prove[Proposition["De Morgan for ∧"]]

Proposition["Switched De Morgan for ∧",
	({{(¬  (A  ∧  
                        B) ) ⇔  ( (¬ B) ∨ (¬ A)), "ma"}})]

Prove[Proposition["Switched De Morgan for ∧"]]

Proposition["De Morgan for ∨",
	({{(¬  (A  ∨  
                        B) ) ⇔  ( (¬ A) ∧ (¬ B)), "mo"}})]

Prove[Proposition["De Morgan for ∨"]]

Proposition["Switched De Morgan for ∨",
	({{(¬  (A  ∨  
                        B) ) ⇔  ( (¬ B) ∧ (¬ A)), "mo"}})]

Prove[Proposition["Switched De Morgan for ∨"]]

Propositional Theorems on Implication

Proposition["Implication by disjunction",
	({{(A⟹
                    B)⟺((¬ A) ∨ 
                    B), "id"}})]

Prove[Proposition["Implication by disjunction"]]

Proposition["Negated implication",
	({{(¬ (A⟹
                        B))⟺(A ∧ (¬ B)), "ni"}})]

Prove[Proposition["Negated implication"]]

Proposition["Contraposition",
	({{(A⟺
                    B)⟺((¬ A)⟺(¬ B)), "cp"}})]

Prove[Proposition["Contraposition"]]

Proposition["Iterated implication",
	({{(A1⟹(A2⟹
                        B))⟺((A1 ∧ 
                        A2)⟹B), "ii"}})]

Prove[Proposition["Iterated implication"], 
      ProverOptions -> {BackChaining -> True}]

Proposition["Distributivity over disjunction",
	({{((A1 ∨ A2)⟹
                    B)⟺((A1⟹B) ∧ (A2⟹B)), "dd"}})]

Prove[Proposition["Distributivity over disjunction"]]

Proposition["Distributivity over conjunction",
	({{((A1 ∧ A2)⟹
                    B)⟺((A1⟹B) ∨ (A2⟹B)), "dc"}})]

Prove[Proposition["Distributivity over conjunction"]]

Proposition["Multiple implication",
	({{(((A1 ∧ A2)⟹
                        B) ∧ (C⟹
                        A1) ∧ (C⟹
                        A2))⟹(C⟹B), "mi"}})]

Prove[Proposition["Multiple implication"], 
      ProverOptions -> {BackChaining -> True}]

Proposition["Multiple conjunction",
	({{(A1 ∧ 
                    A2)⟹(A3⟹(A1 ∧ A2 ∧ A3)), "mc"}})]

Prove[Proposition["Multiple conjunction"]]

Proposition["Redundant implication",
	({{(A⟹(A⟹
                        B))⟺(A⟹B), "ri"}})]

Prove[Proposition["Redundant implication"]]

Proposition["Peirce implication",
	    ({{((A⟹B)⟹
                    A)⟹A, "pi"}})]

Prove[Proposition["Peirce implication"]]

Proposition["Equivalence by implication",
	({{(A⟺
                    B)⟺((A⟹B) ∧ (B⟹A)), "ei"}})]

Prove[Proposition["Equivalence by implication"]]

Proposition["Equivalence by disjunction",
	({{(A⟺
                    B)⟺((A ∧ 
                        B) ∨ ((¬ A) ∧ (¬ B))), "ed"}})]

Prove[Proposition["Equivalence by disjunction"]]

Proposition["Equivalence by conjunction",
	({{(A⟺
                    B)⟺((A ∨ (¬ B)) ∧ ((¬ A) ∨ B)), "ec"}})]

Prove[Proposition["Equivalence by conjunction"]]

This proof is simpler because the rule for proof by cases is used before the rule for transforming implications and equivalences into disjunctions.

Proposition["Negated equivalence",
	({{(¬ (A⟺
                        B))⟺((¬ A)⟺B), "ne"}})]

Prove[Proposition["Negated equivalence"]]

Pelletier Collection

From: F. J. Pelletier, "Seventy-Five Problems for Testing Automatic Theorem Provers", J. of Automated Reasoning, 1986, pp. 191-216

(Only the propositional examples are listed here.)

Problem 1.

Proposition["p1",
	({{(P⟹
                    Q)⟺((¬ Q)⟹(¬ P)), "p1"}})]

Prove[Proposition["p1"]]

Problem 2.

Proposition["p2",
	({{(¬ ¬ P)⟺P, "p2"}})]

Prove[Proposition["p2"]]

Problem 3.

Proposition["p3",
	({{(¬ (P⟹
                        Q))⟹(Q⟹P), "p3"}})]

Prove[Proposition["p3"]]

Problem 4.

Proposition["p4",
	({{((¬ P)⟹
                    Q)⟺((¬ Q)⟹P), "p4"}})]

Prove[Proposition["p4"]]

Problem 5.

Proposition["p5",
	({{((P ∨ Q)⟹(P ∨ 
                        R))⟹(P ∨ (Q⟹R)), "p5"}})]

Prove[Proposition["p5"]]

Prove[Proposition["p5"], 
      ProverOptions -> {TrySubgoal -> True}]

Problem 6. Law of Excluded Middle

Proposition["p6",
	({{P ∨ (¬ P), "p6"}})]

Prove[Proposition["p6"]]

Problem 7. Extended Law of Excluded Middle

Proposition["p7",
	({{P ∨ (¬ ¬ ¬ P), "p7"}})]

Prove[Proposition["p7"]]

Problem 8. Pierce

Proposition["p8",
	({{((P⟹Q)⟹
                    P)⟹P, "p8"}})]

Prove[Proposition["p8"]]

Problem 9.

Proposition["p9",
	({{((P ∨ Q) ∧ ((¬ P) ∨ 
                        Q) ∧ (P ∨ (¬ Q)))⟹(¬ ((¬ P) ∨ (¬ Q))), "p9"}})]

Prove[Proposition["p9"]]

Problem 10.

Proposition["p10 conclusion",
	({{P⟺Q, "p10c"}})]

Proposition["p10 assumptions",
	({{Q⟹R, "p10a1"}, {R⟹(P ∧ Q), "p10a2"}, {P⟹(Q ∨ R), "p10a3"}})]

Prove[Proposition["p10 conclusion"], 
      using -> Proposition["p10 assumptions"]]

Problem 11.

Proposition["p11",
	({{P⟺P, "p11"}})]

Prove[Proposition["p11"]]

Problem 12.

Proposition["p12",
	({{((P⟺
                        Q)⟺
                    R)⟺(P⟺(Q⟺R)), "p12"}})]

Prove[Proposition["p12"]]

Prove[Proposition["p12"], 
      ProverOptions -> {BackChaining -> True}]

\(The\ next\ proof\ was\ nicer\ if\ the\ rule\ "prove by cases"\ was\ applied\ \(\(earlier\)\(.\)\)\)

Proposition["p13",
	({{(P ∨ (Q ∧ 
                        R))⟺((P ∨ 
                        Q) ∧ (P ∨ R)), "p13"}})]

Prove[Proposition["p13"]]

Proposition["p14",
	({{(P⟺
                    Q)⟺((Q ∨ (¬ P)) ∧ ((¬ Q) ∨ P)), "p14"}})]

Prove[Proposition["p14"]]

Proposition["p15",
	({{(P⟹
                    Q)⟺((¬ P) ∨ 
                    Q), "p15"}})]

Prove[Proposition["p15"]]

Proposition["p16",
	({{(P⟹
                    Q) ∨ (Q⟹P), "p16"}})]

Prove[Proposition["p16"]]

Proposition["p17",
	({{((P ∧ (Q⟹
                            R))⟹
                    S)⟺(((¬ P) ∨ 
                        Q ∨ 
                        S) ∧ ((¬ P) ∨ (¬ R) ∨ S)), "p17"}})]

Prove[Proposition["p17"]]