Propositional logic

From Automated Assistance for Formal Reasoning

Propositional logic is supported by the verifier for English phrase predicates that take no arguments. In other words, atoms for propositional logic are defined as English phrase predicates that contain no subexpressions.

[edit] Axioms

We demonstrate that all of the axioms of propositional logic (a list of which can be found in any textbook on logic [1]) are verified by the system under the propositional calculus verification option.

Assert A implies A.

Assert A implies (B implies A).

Assert (A implies B) implies ((A implies (B implies C)) implies (A implies C)).

Assert A implies (B implies (A and B)).

Assert (A and B) implies A.

Assert (A and B) implies B.

Assert A implies (A or B).

Assert B implies (A or B).

Assert (A implies C) implies ((B implies C) implies ((A or B) implies C)).

Assert (not not A) implies A.

Assert (A implies B) implies ((A implies not B) implies not A).

The following corresponds to modus ponens.

Assert ((A implies B) and A) implies B.

[edit] Examples

The search algorithm allows for verification of a variety of more complex propositions.

Assert (A and B and C and D) implies B.

Assert (A implies C) and (B implies C) and (D implies C) implies ((A or B or D) implies C).

[edit] References

[1] Kleene, S. C. Mathematical Logic. New York: Dover, 2002.