LARA

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 

formDecider is invoked using the following command:

jahob/bin/formDecider.opt killer.form -usedp spass

The last argument denote the theorem prover invoked. It can also be:

formDecider.opt killer.form -usedp e
formDecider.opt killer.form -usedp vampire
formDecider.opt killer.form -usedp cvcl
formDecider.opt killer.form -usedp z3

The theorem provers that formDecider invokes are: