Princeton University
Computer Science Dept.

Seminar in Automated Theorem Proving

Homework 4

Investigate the prover. Try some of these first: 
#query test P >- nil --> neg false.

#query test P >- nil -->
    (forall a\ (forall b\ ((q a or q b) imp (exist X \ (q X))))).

#query test P >- nil --> 
     (forall x\ (forall y\
		  (((eq x (plus y (const 0))) and (eq y (const 2))) imp
		   (eq x (const 2))))).

#query test P >- nil --> 
   (forall x\ (forall y\ (forall z\
		  (((eq y (minus z (const ~4))) and
		    (eq (plus x (const 0))
			(minus z (minus (const 3) (plus (const 2)
							(const 4))))))
		   imp (greater (plus y (const 1)) (minus x (const 1))))))).
Then see what it will take for the prover to prove this: 
#query test 
  (pi M\
    P M >- nil --> 
      let_upd M (const 3) (const 4) M\ 
        let upd M (const 4) (const 7) M\
          greater (M(M(const 3))) (M(const 3))
  ).