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.

[CL] Remark. The module Mlogicpa in the file mlogicpa.cl contains built-in properties of the pre-defined functions and predicates in the system CL. Also it contains the syntax of arithmetic tableau rules.

[CL] Remark. In the following examples we recommend to use the pseudo-command open to force the opening of the definitions of defined functions and predicates.

Chapter. Numeric Programs.

Section. Explicit Definitions.

Example of a definition with negation discrimination.

f (x, y) = 0 \leftarrow x = y

f (x, y) = 1 \leftarrow x \neq y

Exercise. Prove

f (x, y) = 0 \lor f (x, y) = 1

Hint. Use cut rule with the cut formula $x = y$ .

f (x, y) = 0 \lor f (x, y) = 1

[CL] Monadic case analysis. Syntax:

case N ; <term>

Example(s):

$case N; t$
$\frac{}{t = 0 ∣ t = x + 1}$
where $x$ is a new variable (eigen-variable).

[CL] Remark. Note that the predicate $N$ is defined in the module Standard as:

N (0)

N (x + 1) \leftarrow N (x)

The proof1 system uses such predicates (you can define your own ones) for the construction of case rules. Try typing just case and the system gives you the full list of case commands available in the current context.

Example of a definition with discrimination on monadic patterns.

f (0) = 0

f (x + 1) = 1

Exercise. Prove

f (x) = 0 \lor f (x) = 1

Hint. Use monadic case analysis on $x$ .

f (x) = 0 \lor f (x) = 1

[CL] Dichotomy case analysis. Syntax:

case Dich ; <term>,<term>

Example(s):

$case Dich; s, t$
$\frac{}{s \leq t ∣ s > t}$

Note that the predicate $Dich$ is defined in the module Standard.

Example of a definition with dichotomy discrimination.

f (x, y) = 0 \leftarrow x ≦ y

f (x, y) = 1 \leftarrow x > y

Exercise. Prove

f (x, y) = 0 \lor f (x, y) = 1

Hint. Use dichotomy case analysis.

f (x, y) = 0 \lor f (x, y) = 1

[CL] Trichotomy case analysis. Syntax:

case Trich ; <term>,<term>

Example(s):

$case Trich; s, t$
$\frac{}{s < t ∣ s = t ∣ s > t}$

Note that the predicate $Trich$ is defined in the module Standard.

Example of a definition with trichotomy discrimination.

f (x, y) = 0 \leftarrow x < y

f (x, y) = 1 \leftarrow x = y

f (x, y) = 2 \leftarrow x > y

Exercise. Prove

f (x, y) = 0 \lor f (x, y) = 1 \lor f (x, y) = 2

Hint. Use trichotomy case analysis.

f (x, y) = 0 \lor f (x, y) = 1 \lor f (x, y) = 2

Minimum.

\min (x, y) = x \leftarrow x ≦ y

\min (x, y) = y \leftarrow x > y

Exercise. Prove

\min (x, y) ≦ x \land \min (x, y) ≦ y \land (\min (x, y) = x \lor \min (x, y) = y)

\min (x, y) ≦ x \land \min (x, y) ≦ y \land (\min (x, y) = x \lor \min (x, y) = y)

Exercise. Find an explicit definition of the maximum function $\max (x, y)$ satisfying

\max (x, y) ≧ x \land \max (x, y) ≧ y \land (\max (x, y) = x \lor \max (x, y) = y)

Prove that the function has the required properties.

\max (x, y) = ?

\max (x, y) ≧ x \land \max (x, y) ≧ y \land (\max (x, y) = x \lor \max (x, y) = y)

Exercise. Prove

\min (x, y) ≦ \max (x, y)

\min (x, y) = \max (x, y) \leftrightarrow x = y

\min (x, y) ≦ \max (x, y)

\min (x, y) = \max (x, y) \leftrightarrow x = y

Exercise. Find an explicit definition of the ternary function ${Min}_{3} (x, y, z)$ satisfying

{Min}_{3} (x, y, z) ≧ x \land {Min}_{3} (x, y, z) ≧ y \land {Min}_{3} (x, y, z) ≧ z

{Min}_{3} (x, y, z) = x \lor {Min}_{3} (x, y, z) = y \lor {Min}_{3} (x, y, z) = z

Prove that the function has the required properties.

{Min}_{3} (x, y, z) = ?

{Min}_{3} (x, y, z) ≦ x \land {Min}_{3} (x, y, z) ≦ y \land {Min}_{3} (x, y, z) ≦ z

{Min}_{3} (x, y, z) = x \lor {Min}_{3} (x, y, z) = y \lor {Min}_{3} (x, y, z) = z

Exercise. Find an explicit definition of the ternary function ${Max}_{3} (x, y, z)$ satisfying

{Max}_{3} (x, y, z) ≧ x \land {Max}_{3} (x, y, z) ≧ y \land {Max}_{3} (x, y, z) ≧ z

{Max}_{3} (x, y, z) = x \lor {Max}_{3} (x, y, z) = y \lor {Max}_{3} (x, y, z) = z

Prove that the function has the required properties.

{Max}_{3} (x, y, z) = ?

{Max}_{3} (x, y, z) ≧ x \land {Max}_{3} (x, y, z) ≧ y \land {Max}_{3} (x, y, z) ≧ z

{Max}_{3} (x, y, z) = x \lor {Max}_{3} (x, y, z) = y \lor {Max}_{3} (x, y, z) = z

Exercise. Find an explicit definition of the function $Median (x, y, z)$ satisfying

x ≦ y \land y ≦ z \to Median (x, y, z) = y

Median (x, y, z) = Median (y, x, z)

Median (x, y, z) = Median (x, z, y)

Prove that the function has the required properties.

Median (x, y, z) = ?

x ≦ y \land y ≦ z \to Median (x, y, z) = y

Median (x, y, z) = Median (y, x, z)

Median (x, y, z) = Median (x, z, y)