Exercise 5.4
(Click "Prove" to run)
Premises:
; There are four nodes represented by n1, n2, n3 and n4 ; There are no other nodes than these (forall ?X (or (= ?X n1) (= ?X n2) (= ?X n3) (= ?X n4))) ; Nodes n1 and n2 are marked ; Nodes n3 and n4 are unmarked (P n1) (P n2) (not (P n3)) (not (P n4)) ; Each of these node labels is distinct from the others (not (= n1 n2)) (not (= n1 n3)) (not (= n1 n4)) (not (= n2 n3)) (not (= n2 n4)) (not (= n3 n4)) ; The graph is a simple cycle through the four nodes (R n1 n2) (R n2 n3) (R n3 n4) (R n4 n1) ; Successors are unique to their predecessor (forall (?X ?Y ?Z) (=> (and (R ?X ?Y) (R ?X ?Z)) (= ?Y ?Z))) ; Predecessors are unique to their successor (forall (?X ?Y ?Z) (=> (and (R ?Y ?X) (R ?Z ?X)) (= ?Y ?Z)))
Conclusion:
; Prove that the following formula is true ; in the structure of exercise 2.1 ; when ?X is n1 ; (and ; (not (R ?X ?X)) ; (not (R n2 ?X)) ; (not (R ?X n3)) ; (P ?X)) (and (not (R n1 n1)) (not (R n2 n1)) (not (R n1 n3)) (P n1))
Proof Trace