Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 17 May 1993 19:39:58 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25777; Mon, 17 May 93 11:19:23 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA25772; Mon, 17 May 93 11:19:08 -0700 Message-Id: <9305171819.AA25772@ted.cs.uidaho.edu> Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) id <00576-0@iraun1.ira.uka.de>; Mon, 17 May 1993 18:28:39 +0200 Date: Mon, 17 May 93 18:29:52 MET DST From: schneide To: info-hol@ted.cs.uidaho.edu Subject: First-Order Reasoning ============================ First-Order Reasoning in HOL ============================ Reasoning in first-order logic can be roughly described as follows: First the formula which is to be proven is negated and skolemized. Then it is to be proven that the resulting formula is unsatisfiable. Therefore, a finite number of instantiations of the quantified formulae has to be performed and afterwards a simple tautology checker is sufficient for the remaining proof. The instantiations can be computed by an external first-order prover. We use our implementation of the FAUST-prover presented a the last HOL workshop. After the prover has computed the instantiations, a HOL proof can be easily done by the following tactics: NEG_SKOLEM_TAC: Negates and skolemizes the given goal DEEP_INSTANCE_TAC [(q1,[t11,...,t1n1]), ..., (qm,[tm1,...,tmnm]) instantiates the quantified subformulae q1,...,qm of the formula PHI(q1,...,qm) on the goal stack by the terms [t11,...,t1n1],... [tm1,...,tmnm], respectively. pp_TAUT_TAC: A tautology checker As already mentioned, we implemented the above tactics for the validation of proofs done by external first-order provers such as FAUST. However, these tactics turned out to be quite useful for interactive theorem proving as well. They can also be used to make some obvious instantiations before the external prover is used (this way we can prove Schubert's Steamroller problem which is still a challenge problem for first-order provers). For illustration, consider the following puzzle, which is proved in HOL below: Someone who lives in Dreadsbury Mansion killed aunt Agatha. Agatha, the butler, and Charles live in Dreadsbury Mansion, and are the only people who live therein. A killer always hates his victim, and is never richer than his victim. Charles hates no one that aunt Agatha hates. Agatha hates everyone except the butler. The butler hates everyone not richer than aunt Agatha and the butler hates everyone that Agatha hates. No one hates everyone and Agatha is not the butler. Who killed aunt Agatha? Answer: Agatha killed herself. A formalisation in HOL would be the following (given by Manthey and Bry): (--`lives agatha /\ lives butler /\ lives charles /\ (killed agatha agatha \/ killed butler agatha \/ killed charles agatha) /\ (!x y. killed x y ==> hates x y /\ ~(richer x y)) /\ (!x. hates agatha x ==> ~(hates charles x)) /\ (hates agatha agatha /\ hates agatha charles) /\ (!x. lives x /\ ~(richer x agatha) ==> hates butler x) /\ (!x. hates agatha x ==> hates butler x) /\ (!x. ~(hates x agatha) \/ ~(hates x butler) \/ ~(hates x charles)) ==> killed agatha agatha`--) The result of the negation and transformation in skolem normal form is the following: (--`~((lives agatha /\ lives butler /\ lives charles /\ (killed agatha agatha \/ killed butler agatha \/ killed charles agatha) /\ (!x y. ~(killed x y) \/ hates x y /\ ~(richer x y)) /\ (!x. ~(hates agatha x) \/ ~(hates charles x)) /\ (hates agatha agatha /\ hates agatha charles) /\ (!x. (~(lives x) \/ richer x agatha) \/ hates butler x) /\ (!x. ~(hates agatha x) \/ hates butler x) /\ (!x. ~(hates x agatha) \/ ~(hates x butler) \/ ~(hates x charles))) /\ ~(killed agatha agatha))`--) Now the following instantiations have to be performed: e(DEEP_INSTANCE_TAC [(--`!x.!y:'a. ~(killed (x:'a) y) \/ hates x y /\ ~(richer x y)`--, [(--`charles:'a`--),(--`butler:'a`--)]) ]); e(DEEP_INSTANCE_TAC [(--`!y:'a. ~(killed (charles:'a) y) \/ hates charles y /\ ~(richer charles y)`--, [(--`agatha:'a`--)]), (--`!y:'a. ~(killed (butler:'a) y) \/ hates butler y /\ ~(richer butler y)`--, [(--`agatha:'a`--)]) ]);OK.. 1 subgoal: (--`~((lives agatha /\ lives butler /\ lives charles /\ (killed agatha agatha \/ killed butler agatha \/ killed charles agatha) /\ ((!y. ~(killed charles y) \/ hates charles y /\ ~(richer charles y)) /\ (!y. ~(killed butler y) \/ hates butler y /\ ~(richer butler y)) /\ T) /\ (!x. ~(hates agatha x) \/ ~(hates charles x)) /\ (hates agatha agatha /\ hates agatha charles) /\ (!x. (~(lives x) \/ richer x agatha) \/ hates butler x) /\ (!x. ~(hates agatha x) \/ hates butler x) /\ (!x. ~(hates x agatha) \/ ~(hates x butler) \/ ~(hates x charles))) /\ ~(killed agatha agatha))`--) ============================= val it = () : unit e(DEEP_INSTANCE_TAC [(--`!x:'a. ~(hates (agatha:'a) x) \/ ~(hates charles x)`--, [(--`agatha:'a`--)]) ]);OK.. 1 subgoal: (--`~((lives agatha /\ lives butler /\ lives charles /\ (killed agatha agatha \/ killed butler agatha \/ killed charles agatha) /\ (((~(killed charles agatha) \/ hates charles agatha /\ ~(richer charles agatha)) /\ T) /\ ((~(killed butler agatha) \/ hates butler agatha /\ ~(richer butler agatha)) /\ T) /\ T) /\ (!x. ~(hates agatha x) \/ ~(hates charles x)) /\ (hates agatha agatha /\ hates agatha charles) /\ (!x. (~(lives x) \/ richer x agatha) \/ hates butler x) /\ (!x. ~(hates agatha x) \/ hates butler x) /\ (!x. ~(hates x agatha) \/ ~(hates x butler) \/ ~(hates x charles))) /\ ~(killed agatha agatha))`--) ============================= val it = () : unit e(DEEP_INSTANCE_TAC [(--`!x:'a. (~(lives x) \/ richer x (agatha:'a)) \/ hates (butler:'a) x`--, [(--`butler:'a`--)]) ]);OK.. 1 subgoal: (--`~((lives agatha /\ lives butler /\ lives charles /\ (killed agatha agatha \/ killed butler agatha \/ killed charles agatha) /\ (((~(killed charles agatha) \/ hates charles agatha /\ ~(richer charles agatha)) /\ T) /\ ((~(killed butler agatha) \/ hates butler agatha /\ ~(richer butler agatha)) /\ T) /\ T) /\ ((~(hates agatha agatha) \/ ~(hates charles agatha)) /\ T) /\ (hates agatha agatha /\ hates agatha charles) /\ (!x. (~(lives x) \/ richer x agatha) \/ hates butler x) /\ (!x. ~(hates agatha x) \/ hates butler x) /\ (!x. ~(hates x agatha) \/ ~(hates x butler) \/ ~(hates x charles))) /\ ~(killed agatha agatha))`--) ============================= val it = () : unit e(DEEP_INSTANCE_TAC OK.. [(--`!x:'a. ~(hates (agatha:'a) x) \/ (hates butler x)`--, [(--`agatha:'a`--),(--`charles:'a`--)]) ]);1 subgoal: (--`~((lives agatha /\ lives butler /\ lives charles /\ (killed agatha agatha \/ killed butler agatha \/ killed charles agatha) /\ (((~(killed charles agatha) \/ hates charles agatha /\ ~(richer charles agatha)) /\ T) /\ ((~(killed butler agatha) \/ hates butler agatha /\ ~(richer butler agatha)) /\ T) /\ T) /\ ((~(hates agatha agatha) \/ ~(hates charles agatha)) /\ T) /\ (hates agatha agatha /\ hates agatha charles) /\ (((~(lives butler) \/ richer butler agatha) \/ hates butler butler) /\ T) /\ (!x. ~(hates agatha x) \/ hates butler x) /\ (!x. ~(hates x agatha) \/ ~(hates x butler) \/ ~(hates x charles))) /\ ~(killed agatha agatha))`--) ============================= val it = () : unit e(DEEP_INSTANCE_TAC [(--`!x:'a. ~(hates x (agatha:'a)) \/ ~(hates x butler) \/ ~(hates x charles)`--, [(--`butler:'a`--)]) ]);OK.. 1 subgoal: (--`~((lives agatha /\ lives butler /\ lives charles /\ (killed agatha agatha \/ killed butler agatha \/ killed charles agatha) /\ (((~(killed charles agatha) \/ hates charles agatha /\ ~(richer charles agatha)) /\ T) /\ ((~(killed butler agatha) \/ hates butler agatha /\ ~(richer butler agatha)) /\ T) /\ T) /\ ((~(hates agatha agatha) \/ ~(hates charles agatha)) /\ T) /\ (hates agatha agatha /\ hates agatha charles) /\ (((~(lives butler) \/ richer butler agatha) \/ hates butler butler) /\ T) /\ ((~(hates agatha agatha) \/ hates butler agatha) /\ (~(hates agatha charles) \/ hates butler charles) /\ T) /\ (!x. ~(hates x agatha) \/ ~(hates x butler) \/ ~(hates x charles))) /\ ~(killed agatha agatha))`--) ============================= val it = () : unit e(pp_TAUT_TAC); OK.. Proof by abstracting to propositional logic: ~((p1 /\ p2 /\ p3 /\ (p4 \/ p5 \/ p6) /\ (((~p6 \/ p7 /\ ~p8) /\ p9) /\ ((~p5 \/ p10 /\ ~p11) /\ p9) /\ p9) /\ ((~p12 \/ ~p7) /\ p9) /\ (p12 /\ p13) /\ (((~p2 \/ p11) \/ p14) /\ p9) /\ ((~p12 \/ p10) /\ (~p13 \/ p15) /\ p9) /\ (~p10 \/ ~p14 \/ ~p15) /\ p9) /\ ~p4) Goal proved.... Has anybody similar tactics or conversions?