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. Numeric Programs.

Section. Explicit Definitions.

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

x < y \lor x ≧ z \to f (x, y, z) = 1

\neg (x < y \lor x ≧ z) \to f (x, y, z) = 2

Prove that the function has the required properties. Otherwise, show that there is no such function.

f (x, y, z) = ?

x < y \lor x ≧ z \to f (x, y, z) = 1

\neg (x < y \lor x ≧ z) \to f (x, y, z) = 2

x < y \lor x ≧ z \to f (x, y, z) = 1

\neg (x < y \lor x ≧ z) \to f (x, y, z) = 2

⊥

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

x < y + z \lor x > y \land x > z \to f (x, y, z) = 1

\neg (x < y + z \lor x > y \land x > z) \to f (x, y, z) = 2

Prove that the function has the required properties. Otherwise, show that there is no such function.

f (x, y, z) = ?

x < y + z \lor x > y \land x > z \to f (x, y, z) = 1

\neg (x < y + z \lor x > y \land x > z) \to f (x, y, z) = 2

x < y + z \lor x > y \land x > z \to f (x, y, z) = 1

\neg (x < y + z \lor x > y \land x > z) \to f (x, y, z) = 2

⊥

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

x > y \to f (x, y, z) = 1

x > z \to f (x, y, z) = 2

\neg (x > y \lor x > z) \to f (x, y, z) = 3

Prove that the function has the required properties. Otherwise, show that there is no such function.

f (x, y, z) = ?

x > y \to f (x, y, z) = 1

x > z \to f (x, y, z) = 2

\neg (x > y \lor x > z) \to f (x, y, z) = 3

x > y \to f (x, y, z) = 1

x > z \to f (x, y, z) = 2

\neg (x > y \lor x > z) \to f (x, y, z) = 3

⊥

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

x > y + z \to f (x, y, z) = 1

x < y \to f (x, y, z) = 2

\neg (x > y + z \lor x < y) \to f (x, y, z) = 3

Prove that the function has the required properties. Otherwise, show that there is no such function.

f (x, y, z) = ?

x > y + z \to f (x, y, z) = 1

x < y \to f (x, y, z) = 2

\neg (x > y + z \lor x < y) \to f (x, y, z) = 3

x > y + z \to f (x, y, z) = 1

x < y \to f (x, y, z) = 2

\neg (x > y + z \lor x < y) \to f (x, y, z) = 3

⊥

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

x < y + z \to f (x, y, z) = 1

x > y \to f (x, y, z) = 2

\neg (x < y + z \lor x > y) \to f (x, y, z) = 3

Prove that the function has the required properties. Otherwise, show that there is no such function.

f (x, y, z) = ?

x < y + z \to f (x, y, z) = 1

x > y \to f (x, y, z) = 2

\neg (x < y + z \lor x > y) \to f (x, y, z) = 3

x < y + z \to f (x, y, z) = 1

x > y \to f (x, y, z) = 2

\neg (x < y + z \lor x > y) \to f (x, y, z) = 3

⊥