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

Literature.

[1] Ján Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
[3] Ján Komara. Recursive Functions. Online.

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. (1 point) 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

[CL] Propositional logic with automatic 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. (1 point) The merchant McGregor was robbed. There were four suspects $X$ , $Y$ , $Z$ , and $W$ . The following facts were unearthed by Inspector Lestrade:

(1) If $X$ is guilty, then $Y$ was his companion.
(2) If $Y$ is guilty, then at least one of $X$ and $Z$ is not guilty.
(3) If $W$ is guilty, then so are $X$ and $Z$ .
(4) If $X$ is not guilty, then $W$ is guilty.

Decide the guiltiness of each person involved.

G (X) \to G (Y)

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

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

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

⊥