Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)

Literature.

[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

Chapter. Propositional Logic.

Section. Language.

Formulas.

[CL] Syntax. Examples:

Atomic formulas: $R$ , $Q$ .
Propositional connectives: $⊤$ , $⊥$ , $\neg R$ . $R \land Q$ , $R \lor Q$ , $R \to Q$ , $R \leftrightarrow Q$ .

Section. The Method of Propositional Tableaux.

[CL] Remark. The module Mlogicp in the file mlogicp.cl contains the syntax of propositional tableau rules.

A

B

C

Exercise. Prove that logical disjunction is distributive over logical conjunction:

A \lor B \land C \leftrightarrow (A \lor B) \land (A \lor C)

A \lor B \land C \leftrightarrow (A \lor B) \land (A \lor C)

Exercise. Prove that logical implication is transitive:

(A \to B) \land (B \to C) \land A \to C

(A \to B) \land (B \to C) \land A \to C

Exercise. Prove that contrapositives of logical implication are logically equivalent:

(A \to B) \leftrightarrow \neg B \to \neg A

(A \to B) \leftrightarrow \neg B \to \neg A