Clausal Language (ver. 5.81.21, 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 \to (A \lor B) \land (A \lor C)

A \lor B \land C \to (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

Section. Tableaux with Axioms.

[CL] Remark. The module Mlogicpx in the file mlogicpx.cl contains the syntax of tableau rules for propositional tableaux with axioms. The module Mlogicd in the file mlogicd.cl contains the syntax of derived tableau rules.

Remark. The following logical problems are from the cases solved by the famous inspector G. Lestrade of Scotland Yard.

Exercise. Investigation by Inspector Lestrade brought up the following facts:

(1) The robbery was done by at least by $X$ , $Y$ , or $Z$ .
(2) $X$ always works with a companion.
(3) $Z$ is not guilty.

Problem: Is $Y$ guilty?

Formalization.

The constants $X$ , $Y$ a $Z$ represent the suspects.
The predicate $G (x)$ holds if $x$ is guilty.

The axioms A1, A2 a A3 arithmetize the facts (1), (2) a (3). Our goal is to prove that the claim $G (Y)$ is a tautological consequence of these axioms.

G (X) \lor G (Y) \lor G (Z)

G (X) \to G (Y) \lor G (Z)

\neg G (Z)

G (Y)

Exercise. What are the consequences of the following facts?

(1) If $X$ is guilty and $Y$ is not then $Z$ is guilty.
(2) $Z$ never works alone.
(3) $X$ never works with $Z$ .
(4) Except $X$ , $Y$ , or $Z$ nobody else is involved in the case.

Decide the guiltiness of each person involved, i.e. prove whether G(x) or $\neg G (x)$ for every $x = X, Y, Z$ .

G (X) \land \neg G (Y) \to G (Z)

G (Z) \to G (X) \lor G (Y)

\neg (G (X) \land G (Z))

G (X) \lor G (Y) \lor G (Z)

Exercise. The merchant McGregor was robbed. There were three suspects $X$ , $Y$ , and $Z$ . The following facts were unearthed:

(1) All suspects and nobody else was that day in McGregor's store.
(2) If $X$ is guilty then he worked with a companion.
(3) $Y$ is guilty if and only if $Z$ is guilty.

Decide the guiltiness of each person involved.

G (X) \lor G (Y) \lor G (Z)

G (X) \to G (Y) \lor G (Z)

G (Y) \leftrightarrow G (Z)

Exercise. In a police case the following was found out:

(1) If $X$ is guilty then $Y$ was his companion.
(2) If $Y$ is guilty then either $X$ is not or $Z$ is guilty.
(3) If $W$ is guilty then $X$ is and $Z$ is not.
(4) If $X$ is not guilty then $W$ is.

Decide the guiltiness of each person involved.

G (X) \to G (Y)

G (Y) \to G (Z) \lor \neg G (X)

G (W) \to G (X) \land \neg G (Z)

\neg G (X) \to G (W)