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] CL-TeX.

Starting CL.

Part I. Evaluation.

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.

Part II. Function Definitions.

[CL] Syntax. Identifier conventions:

Variable identifier. A string of lower case letters possibly followed by one or two digits as indices. Examples: $x$ , $ys$ , $i_{1}$ , ${foo}_{99}$ .
Function identifier. An alpha-numeric string starting with a capital letter and containing lower case letters, digits, and underline symbols '_'. Examples: $F$ , $Max$ , $Power_of_some_prime$ , ${A1b2c}_{3}$ .

[CL] Remark. By a component we mean either remark, or definition or theorem.

Square function. The next component contains the explicit definition of the function $Square (x)$ which yields the square $x^{2}$ of the number $x$ .

Square (x) = x \cdot x

Exercise. Evaluate the square function for some arguments; e.g. execute the query $Square (5) = x$ .

Cube function. Write an explicit definition of the function $Cube (x)$ which yields the cube $x^{3}$ of the number $x$ .

Hint. Use the Ins/Del button.

Sum of two squares. Write an explicit definition of the binary function $Sum_of_squares (x, y)$ which yields the sum of the squares $x^{2}$ and $y^{2}$ .

[CL] Final remark. Save your solutions and exit the system CL. That is, click the Save & Exit button or type Alt + X.

Query:

Heap used: 210816 free: 134005324

Time used: 0:0:0:85