logic QBF

spec testProver1 =

prop a, b, c

. a

. not b

. forall p . p \/ a => a %implied

. forall p . p \/ b => b %implied

. exists p . p /\ c => a %implied

. forall p,d . p /\ d %implied

end

spec testProver2 =

prop a, b

. a

. not b

. (exists p . p <=> a) /\ (exists p . p <=> b) %implied

spec testProver3 =

prop a, b, c

. (exists p . p <=> a /\ (b => c)) \/ (forall d . d => (c => (b => (a <=> (forall e . e <=> b))))) %implied