ϵ">]>
Literature.
[1] Ján Komara. Specification and Verification of Programs. Online.
Chapter. Quantification Logic.
Section. Quantification Tableaux.
[CL] Remark. The module Mlogicq in the file mlogicq.cl contains the syntax of tableau rules for quantifier tableaux.
###
Exercise. Prove the following sentence:
##
Exercise. Prove the following sentences:
Section. Logical Consequence.
[CL] Remark. In the following examples you can use derived quantifier tableau rules as described in the module Mlogicd (see the file mlogicd.cl).
Exercise. Suppose that the binary predicate R (x,y) is symmetric and transitive:
Show that the predicate is reflexive on its domain of definition:
Exercise. (1 bonus point) Suppose that the binary predicate R (x,y) is ireflexive and transitive:
Show that the predicate is asymmetric:
Exercise. (1 bonus point) Suppose that the binary predicate R (x,y) is symmetric and antisymmetric:
Show that the predicate is the identity on its domain of definition:
Exercise. (1 bonus point) Suppose that the binary predicate R (x,y) is equivalence:
Show that the predicate satisfies the property:
Exercise. (3 bonus points) Suppose that the binary predicate R (x,y) satisfies the property:
Show that the predicate is equivalence: