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. 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 exercises are logical problems from the book What is the name of this book? by Raymond Smullyan . The problems are from the cases solved by the famous inspector Nick Fishthrawn of Scotland Yard.

Exercise. Investigation by inspector Fishtrawn 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)