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.

Starting CL.

Exercise. Your task is to use CL as a simple calculator for the evaluation of arithmetic expressions in the form of so-called queries. The window Query which appears at the end is designed for the input of queries. The result of a given query will be displayed in the window Results.

Examples of simple queries:

Addition. Query: $2 + 3 = x$ . CL-syntax is: $2+3 = x$ . Result: true for $x = 5$ .
Modified subtraction. Query: $12 \dot{-} 5 = x$ . CL-syntax is: $12-5 = x$ . Result: true for $x = 7$ .
Multiplication. Query: $5 \cdot 3 = x$ . CL-syntax is: $5*3 = x$ . Result: true for $x = 15$ .
Integer (Euclidean) division. Query: $13 \div 3 = x$ . CL-syntax is: $13/3 = x$ . Result: true for $x = 4$ .
Remainder after integer division. Query: $13 mod 8 = x$ . CL-syntax is: $13 mod 8 = x$ . Result: true for $x = 5$ .

Further apply these queries:

$(2 + 3) \cdot 5 \div 4 = x$
$19 \dot{-} 20 = x$
$2 \div 0 + 3 mod 0 = x$

The last two examples illustrate the following properties of arithmetic operators:

x ≦ y \to x \dot{-} y = 0

x \div 0 = 0 \land x mod 0 = 0

Exercise. It is possible to evaluate also compound queries (conjunctions of simple queries). For instance

2 + 3 = x \land 4 \cdot 5 = y \land x + y \dot{-} 3 = z

CL-syntax is:

2+3 = x & 4*5 = y & x+y-3 = z

Result: true for $x = 5$ , $y = 20$ , and $z = 22$ .

Examples of syntactically incorrect queries (when reading the queries from left to right):

$x = 2 + 3$ . The variable $x$ has not been assigned a value.
$2 + y = x$ . The variable $y$ has not been assigned a value.
$2 + 3 = x \land z = 4 \cdot x$ . The variable $z$ has not been assigned a value.

Exercise. Your next task is to use CL for the evaluation of arithmetic comparison relations.

Examples of simple queries:

Query: $2 + 3 = 1 + 4$ . CL-syntax: $2+3 = 1+4$ . Result: true.
Query: $2 + 3 \neq 1 + 4$ . CL-syntax: $2+3 != 1+4$ . Result: false.
Query: $2 + 3 ≦ 1 + 4$ . CL-syntax: $2+3 <= 1+4$ . Result: true.
Query: $2 + 3 < 1 + 4$ . CL-syntax: $2+3 < 1+4$ . Result: false.
Query: $2 + 3 > 1 + 4$ . CL-syntax: $2+3 > 1+4$ . Result: false.
Query: $2 + 3 ≧ 1 + 4$ . CL-syntax: $2+3 >= 1+4$ . Result: true.

Example of a compound query:

Query: $2 + 3 = x \land 1 + 4 = y \land x ≦ y \land x + 1 > y$ . Result: true.

Examples of syntactically incorrect queries:

$x ≦ 2 + 3$ . The variable $x$ has not been assigned a value.
$2 + 3 = x \land y ≧ 4 \cdot x$ . The variable $y$ has not been assigned a value.

Query:

Heap used: 189768 free: 134026488

Time used: 0:0:0:15