ϵ">]> Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)
...
Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)
Module  Ex02a in logic: Peano arithmetic
Included module  Standard
Remark 

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.

Remark 

Chapter. Quantification Logic.

Remark 

Section. Quantification Tableaux.

Remark 

[CL] Remark. The module Mlogicq in the file mlogicq.cl contains the syntax of tableau rules for quantifier tableaux. The module Mlogicd in the file mlogicd.cl contains the syntax of derived tableau rules. 

###
Theory  Examples in logic: first-order logic
Predicate  R  / 2
Remark 

Exercise. Prove the following sentence:

∃ y ∀ x R ( x , y ) → ∀ x ∃ y R ( x , y ) 
##
Theorem  Exists_forall
∃ y ∀ x R ( x , y ) → ∀ x ∃ y R ( x , y )
Predicate  A
Predicate  B
Remark 

Exercise. Prove the following sentences:

∃ x (A ( x ) ∧B ( x ) ) → ∃ x A ( x ) ∧ ∃ x B ( x ) ∀ x A ( x ) ∨ ∀ x B ( x ) → ∀ x (A ( x ) ∨B ( x ) ) ¬ ∃ x A ( x ) ↔ ∀ x ¬A ( x ) 
##
Theorem  Exists_and
∃ x (A ( x ) ∧B ( x ) ) → ∃ x A ( x ) ∧ ∃ x B ( x ) 
##
Theorem  Forall_or
∀ x A ( x ) ∨ ∀ x B ( x ) → ∀ x (A ( x ) ∨B ( x ) ) 
##
Theorem  Not_exists
¬ ∃ x A ( x ) ↔ ∀ x ¬A ( x )
End of theory  Examples
Query:

Results:
Heap used: 178472 free: 134037904
Time used: 0:0:0:20