LARA

• 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.

• 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:

• e = E theorem prover
• vampire = Vampire theorem prover
• cvcl = CVC3 theorem prover
• z3 = Z3 theorem prover

• Install the Isabelle/HOL theorem prover and test it on “Dreadbury Mansion Mystery” example:

theory aunt
imports Main
begin
theorem agatha:
assumes a1 : "EX  x.(lives(x) & killed(x, a))"
and     a2 : "lives(a) & lives(b) & lives(c) & (ALL x. (lives(x) --> (x=a | x=b | x=c)))"
and     a3 : "ALL x. ALL y. (killed(x,y) --> (hates(x,y) & ~richer(x,y)))"
and     a4 : "ALL x. (hates(a,x) --> ~hates(c,x))"
and     a5 : "ALL x. (hates(a,x) = (x ~= b))"
and     a6 : "ALL x. ((~richer(x,a)) = hates(b,x))"
and     a7 : "ALL x. (hates(a,x) --> hates(b,x))"
and     a8 : "~(EX x. ALL y. hates(x,y))"
and     a9 : "a ~= b"
shows   "killed(a,a)"
using a1 a2 a3 a4 a5 a6 a7 a8 a9 sledgehammer e
end

In the specification we invoke E for proving the formulas.