This is an old revision of the document!
SPASS - First-order theorem prover
- Install SPASS and test it on “Dreadbury Mansion Mystery” example:
begin_problem(aunt_Agatha). list_of_descriptions. name({*Who killed Aunt Agatha?*}). author({*Ruzica Piskac*}). status(unsatisfiable). description({*Well known example of encoding real life problems into FOL*}). end_of_list. list_of_symbols. functions[(a,0),(b,0),(c,0)]. predicates[(lives,1),(killed,2),(richer,2),(hates,2)]. end_of_list. list_of_formulae(axioms). % Someone who lives in Dreadbury Mansion killed Aunt Agatha. formula(exists([X],and(lives(X),killed(X,a)))). % Agatha, the butler, and Charles live in Dreadbury Mansion, and are the only people who live therein. formula(lives(a)). formula(lives(b)). formula(lives(c)). formula(forall([X],implies(lives(X),or(or(equal(X,a),equal(X,b)),equal(X,c))))). % A killer always hates his victim, and is never richer than his victim. formula(forall([X],forall([Y], implies(killed(X,Y),and(hates(X,Y),not(richer(X,Y))))))). % Charles hates no one that Aunt Agatha hates. formula(forall([X],implies(hates(a,X),not(hates(c,X))))). % Agatha hates everyone except the butler. formula(forall([X],equiv(not(equal(X,b)),hates(a,X)))). % The butler hates everyone not richer than Aunt Agatha. formula(forall([X],implies(not(richer(X,a)),hates(b,X)))). % The butler hates everyone Aunt Agatha hates. formula(forall([X],implies(hates(a,X),hates(b,X)))). % No one hates everyone. formula(not(exists([X],forall([Y],hates(X,Y))))). % Agatha is not the butler formula(not(equal(a,b))). end_of_list. list_of_formulae(conjectures). formula(killed(a,a)). end_of_list.
end_problem.
formDecider - part of Jahob
- Install the Jahob system and test it on “Dreadbury Mansion Mystery” example:
(EX x. lives x & killed x a) & (lives :: obj => bool) a & lives b & lives c & (ALL x. lives x --> (x = a | x = b | x = c)) & (ALL x y. killed x y --> hates x y & ~(richer x y)) & (ALL x. hates a x --> ~(hates c x)) & (ALL x. x ~= b --> hates a x) & (ALL x. ~((richer :: obj => obj => bool) x a) --> hates b x) & (ALL x. hates a x --> hates b x) & ~(EX x. (ALL y. hates x y)) & a ~= b --> (killed :: obj => obj => bool) a a