Home
Model Elimination, Logic Programming
Contents
1. ine first part Or the theorem Will be used 1n the proor or refutational completeness because for a refutation on the ground level i e a derivation of P only the empty path set Pa can be more general while the second part will be used in the proof of answer completeness Theo rem 2 3 In particular to obtain this we have to demand one single substitution which maps any of the clauses Cpo used in extension steps to the respective clause on the ground level Clearly this result is harder to establish and more relevant than a lifting result for SLI resolution in Lobo et al 1992 which moves the J quantification inside in our words they state that for every application of an input clause at the ground level there exists an application at the first order level and there exists a substitution to map this instance to the ground level Theorem 2 3 Answer completeness of restart ME If Q6 V V QO is a correct answer for a program P then there exists a strict restart ME refutation from S with computed answer Qo V VQoy such that Qo V VQoy entails Q6 V VQ6 i e J Vi 1 m Jj 1 1 Qoid Qj Informally the theorem states that for every given correct answer we can find a computed answer which can be instanti ated by means of a single substitution 6 to a subclause of the given answer and hence implies it Unfortunately we can not obtain a result stating that the computed answe
2. In this subsection we use the clause notation mirroring the fact that we review a calculus which is as it stands not suited for programming purposes We use a ME calculus that dif fers from the original one presented in Loveland 1968 It a goal Lek OSes LT P Q sP Q oF Ss 7 We x ane 7 IN eS Q P Q P i Q P Q P BOS 4 AN 1 AN a S a P Q ap Q P Q 1 goal AN P Q 7 HOS 1 Q ap Figure 1 Model Elimination left side vs Restart Model Elimina tion right side is described in Letz et al 1992 as the base for the prover SETHEO In Baumgartner and Furbach 1993 this calcu lus is discussed in detail by presenting it in a consolution style Eder 1991 and compared to various other calculi ME in this sense manipulates trees by extension and reduction steps In order to recall the calculus consider the clause set P Q j oP Q Q P P Q A model elimination refutation is depicted in Figure left side It is obtained by successive fanning with clauses from the input set extension steps Additionally it is required that every inner node is complementary to one of its sons Such sons are decorated with a x in Figure 1 A dashed arrow indicates a reduction step i e the closing of a branch due to a path literal complementary to the leaf literal Extension and reduction steps are allowed at any leaf of the tree and for extension steps any literal
3. cation to PTTP Journal of Automated Reasoning 13 339 359 1994 Short version in Proceedings of CADE 12 Springer LNAI 814 1994 pp 87 101 Baumgartner and Furbach 1994b P Baumgartner and U Fur bach PROTEIN A PROver with a Theory Extension nterface In A Bundy editor Automated Deduction CADE 12 volume 814 of LNAI pages 769 773 Springer 1994 Baumgartner et al 1995 Peter Baumgartner Ulrich Furbach and Frieder Stolzenburg Model elimination logic programming and computing answers Fachberichte Informatik 1 95 Universitat Koblenz Landau Koblenz 1995 Baumgartner 1994 P Baumgartner Refinements of Theory Model Elimination and a Variant without Contrapositives In A G Cohn editor 71th European Conference on Artificial Intelligence ECAI 94 Wiley 1994 Long version in Research Report 8 93 University of Koblenz Institute for Computer Science Koblenz Germany ECRC 1994 ECRC GmbH Miinchen ECLiPSe 3 4 User Man ual Extensions User Manual January 1994 Eder 1991 E Eder Consolution and its Relation with Resolution In Proc IJCAI 91 1991 Letz et al 1992 R Letz J Schumann S Bayerl and W Bibel SETHEO A High Performance Theorem Prover Journal of Au tomated Reasoning 8 2 1992 Lobo et al 1992 Jorge Lobo Jack Minker and Arcot Rajasekar Foundations of Disjunctive Logic Programming MIT Press Cam bridge MA London England 1992 Loveland and Reed 1992 D Lovel
4. 2 there is a positive literal L in p such that L leaf p is a connection with MGU The inference rule restart is defined as follows PU p PU po L 1 P U p is a path multiset and where 2 leaf p is a positive literal and 3 L first p A strict restart ME derivation from the clause set S consists of a sequence Po P1 Pn and a substitution 01 On Where 1 Po is a path multiset Li In consisting of paths of length 1 with L V V Ly in S also called the goal clause and fori 1 n 2 Pi is obtained from P _ by means of an extension step with an appropriate clause C from S and MGU 9 or 3 Pi is obtained from P _ by means of a reduction step and MGU o or 4 P is obtained from P _ by means of a restart step The path p is called selected path in all three inference rules A restart step followed immediately by an extension step at the just obtained path is also called a restart extension step Finally a refutation is a derivation where P O Note that in extension steps we can connect only with the head literals of input clauses Since in general this re striction is too strong we have to restart the computa tion with a fresh copy of a negative clause This is achieved by the restart rule because refutations of programs in goal normal form always start with agoal i e the copied lit eral first p goal furthermore only extension steps are possible to goa
5. Model Elimination Logic Programming and Computing Answers Peter Baumgartner Ulrich Furbach Frieder Stolzenburg Universit t Koblenz Institut fiir Informatik Rheinau 1 D 56075 Koblenz Germany E mail peter uli stolzen informatik uni koblenz de Abstract We demonstrate that theorem provers using model elimination ME can be used as answer com plete interpreters for disjunctive logic program ming More specifically we introduce a mechanism for computing answers into the restart variant of ME Building on this we develop a new calculus called ancestry restart ME This variant admits a more restrictive regularity restriction than restart ME and as a side effect it is in particular attrac tive for computing definite answers The presented calculi can also be used successfully in the context of automated theorem proving We demonstrate ex perimentally that it is more difficult to compute non trivial answers to goals instead of only prov ing the existence of answers Keywords Automated reasoning theorem prov ing model elimination logic programming com puting answers The aim of this paper is twofold Firstly we prove that the orem provers using model elimination ME can be used as answer complete interpreters for disjunctive logic program ming Secondly we demonstrate that in the context of auto mated theorem proving it is much more difficult to compute non trivial answers to goals instead of only to
6. THEO Table 2 shows the timings for OTTER and SETHEO All timings are measured on a Sparc 10 The sym bol oo denotes the fact that no proof was found within 1 hour that is true for OTTER applied to case b of our example PROTEIN is answer complete that has been stated in this paper It finds out the indefinite and definite answer for the respective case The table in Figure 2 also shows some tim ings for finding these answers with PROTEIN We tried both plain and restart ME In case of the restart variant we also tried its refinements with or without ancestry restart or se lection function no contrapositives We tried to compute the desired answers with settings where all solutions are com puted in case a indefinite answer For the case b definite answer we used the setting where only definite answers are searched for By this we get a significant speed up of the search As one can see using restart helps for this problem since plain ME does not find the desired answers quickly al though it does so for trivial answers But it is not quite clear which flags should be used in addition We investigated more puzzle examples from Smullyan 1978 All our experiments corroborate the following facts resolution has difficulties in solving puzzles because of the problem with subsumption model elimination is better suited although it could not solve all puzzles that we tested For example OTTER needs 281 8s on puzzle 35 wh
7. The example follows problem 36 in Smullyan 1978 A similar example is studied in Ohlbach 1985 The natural language description of the problem is stated below There the last two pieces of information 5 and 6 explicitly state some knowledge about inferencing We need them in order to be able to cope with the information in 2 because our de scription language is first order 1 On an island there live exactly two types of peo ple knights and knaves 2 Knights always tell the truth and knaves always lie 3 I landed on the is land met two inhabitants asked one of them Is one of you a knight and he answered me 4 What can be said about the types of the asked and the other person depending on the answer I get 5 We assume that either a proposition or its negation is true 6 If the disjunction of two propositions is true then at least one of them must be true In our formalization of the problem below the formulae in 1 and 2 express the corresponding pieces of information from above Depending on the case considered we choose one of the formulae a or b in 3 We view the fact that a person denies a question as that he says that the thing in question is not true using the binary predicate says instead of a ternary predicate Formula 4 can be considered as the query We have to express the pieces of information 5 and 6 explicitly by in troducing the unary predicate true The transformation of the formulae below in
8. and and D Reed Near Horn Prolog and the Ancestry Family of Procedures Technical Report CS 1992 20 Department of Computer Science Duke University Durham North Carolina December 1992 Loveland 1968 D Loveland Mechanical Theorem Proving by Model Elimination JACM 15 2 1968 Loveland 1991 D Loveland Near Horn Prolog and Beyond Journal of Automated Reasoning 7 1 26 1991 Manthey and Bry 1988 Rainer Manthey and Fran ois Bry SATCHMO a theorem prover implemented in Prolog In Ewing Lusk and Ross Overbeek editors Proceedings of the 9th International Conference on Automated Deduction Ar gonne Illinois USA May 1988 pages 415 434 Springer Berlin Heidelberg New York 1988 LNCS 310 UvicCune 1974 William W ivicCune OL LEW 5 U reference man ual and guide Technical Report ANL 94 6 National Laboratory Argonne IL January 1994 Ohlbach 1985 Hans J rgen Ohlbach Predicate logic hacker tricks Journal of Automated Reasoning 1 435 440 1985 Plaisted 1988 D Plaisted Non Horn Clause Logic Program ming Without Contrapositives Journal of Automated Reasoning 4 287 325 1988 Smullyan 1978 Raymond M Smullyan What is the name of this book The riddle of Dracula and other logical puzzles Prentice Hall Englewood Cliffs NJ 1978 Sutcliffe et al 1994 G Sutcliffe C Suttner and T Yemenis The TPTP problem library In Proc CADE 12 Springer 1994
9. es that negative liter als inside blocks are pairwise different where by a block we mean a smallest subpath delimited by positive literals or the ends of the path Condition 3 means that a negative literal may be equal to one of its ancestors only if it follows a positive lit eral i e if it is used as a restart literal Thus we have a global regularity condition except for restart literals In all example refutations given so far all branches are blockwise regular However the refutation in Figure 1 right side is not globally regular as can be seen by the two occurrences of Q in the rightmost path From this example we learn that restart ME is incompatible with the global regularity restriction However it holds Theorem 3 3 Completeness of Ancestry Restart Model Elimination Let f be a head selection function and S be an unsatisfiable clause set in goal normal form Then there exists a glob ally regular ancestry restart ME refutation of S starting with lt goal and selection function f We can use this result to obtain the desired completeness result for definite answers Theorem 3 4 Answer completeness of ancestry restart ME Ancestry restart ME is answer complete in the sense of Theorem 2 3 In particular if Q0 is a correct definite answer for a program P then there exists an ancestry restart ME refutation from P with computed answer Qo such that Qod Q90 for some substitution 6 Furthermore the input clause goal Q i
10. ex ample which illustrates this is case a where the search stops after finding 15 times only the trivial answer with binary res olution However we find a proof by using hyper resolution with factorization immediately within 0 4s There is a solu tion to the problem with subsumption it can be shown that we only have to take the answer literals into account during the subsumption steps Unfortunately it is not yet possible to test OTTER in this setting and find out whether this improves the behaviour because it is not built in OTTER trivial 2 1 plain hyper resolution indefinite 0 4 hyper resolution factor definite le several trials SETHEO trivial 0 5 indefinite 1 0 definite 0 6 5 with constraints with constraints with constraints any setting plain ME restart sel function plain ME ancestry restart PROTEIN trivial 0 indefinite co 41 4 definite 2022 8 38 4 Figure 2 Timings We generate answers with SETHEO by using global vari ables The answers are kept in a list By this and other tech nical tricks we find the indefinite answer within 1 0s and the definite answer within 0 6s That is quite good and may be explained by the subgoal reordering heuristics built into SETHEO which are not yet incorporated into our sys tem But in addition SETHEO also has subsumption con straints which are used in the default setting It is not quite clear whether these constraints destroy answer completeness in SE
11. from an input clause can be used to form a complementary pair of literals For example in the right subtree of Figure 1 left side the clause P Q was used to extend the positive leaf P i e we used the program clause Q P via the body literal P and hence did dissent with a procedural reading of the clause In the right part of Figure 1 a refutation with the modi fied version the restart ME calculus is displayed The only difference is that extension steps at positive literals are not allowed instead either a reduction step is carried out or else the root literal which is always goal is copied and then an extension follows In a variant called strict restart model elimination not even reduction steps are allowed at positive leaves Hence the cal culus is forced to apply restart steps wherever possible These simple modifications obviously allow only extension steps with a positive i e a head literal of a clause and hence support a procedural reading of program clauses In the fol lowing subsection we give a formal presentation of the calcu lus along the lines of Baumgartner and Furbach 1993 1 2 Restart Model Elimination Instead of trees we now manipulate multisets of paths where paths are sequences of literals We will state some basic defi nitions AA CLAUSE 1S a MULLUSEL OF Ulerais USUALLY WIItleN as the dis junction L V VLy A program is a consistent set of clauses thus possibly including negative c
12. ile PRO TEIN only needs 153 1s Further investigations are necessary It seems that also a model generation approach is very ade quate Manthey and Bry 1988 for these kind of problems because they often allow for finite models Last but not least we want to point out that both OTTER and SETHEO do not support a procedural reading of program clauses they need all contrapositives but PROTEIN does and that is useful if we want to use logic as a real programming language 0 VCUHUUSION To conclude it seems to be very promising to use ME as a base calculus for computing answers in disjunctive logic pro gramming In this paper we introduce among others the an cestry restart variant which is quite well suited for this pur pose We also give some practical evidence Nevertheless further investigation is necessary in order to find out yet more efficient calculi and to incorporate nonmonotonic extensions Acknowledgements We would like to thank Francois Bry Jiirgen Dix Bertram Fronhofer Reinhold Letz and William W McCune for help ful discussions and Olaf Menkens and Dorothea Sch fer for their implementational work References Baumgartner and Furbach 1993 P Baumgartner and U Furbach Consolution as a Framework for Comparing Calculi Journal of Symbolic Computation 16 5 1993 Academic Press Baumgartner and Furbach 1994a P Baumgartner and U Fur bach Model Elimination without Contrapositives and its Appli
13. ive these answers we need a clause set which is not minimal unsatisfiable notice that the clauses of 1 and 4 together are minimal unsatisfi able yielding the trivial answer Thirdly 9 extension steps are needed to derive the indefinite or the definite answer respec tively while only 7 extension steps are needed to derive the trivial answer in both cases These remarks indicate that it should be more difficult to find the more precise answers 5 2 Experimental Results We tried to get the answers from above automatically by us ing the theorem proving systems OTTER McCune 1994 which is a resolution style theorem proving program coded in C for first order logic with equality SETHEO Letz et al 1992 which is a top down prover for first order predi cate logic based on the calculus of the so called connection tableaux which generalizes weak ME implemented in C and PROTEIN Baumgartner and Furbach 1994b which we al ready introduced in Section 4 We used the clause ordering given by the problem description but our experiments show that the run time results depend on the ordering OTTER has some problems with computing answers be cause it enumerates resolvents but not all refutational proofs Especially during the subsumption test it did not take the answer literals into account which are provided for com puting answers That is the reason why OTTER with forward and backward subsumption is not answer complete An
14. l introducing a new copy of a negative clause cf Figure 1 right side ine reduction operation 1s permitted trom negative lear Ht erals to positive ancestor literals only This condition can be relaxed towards disregarding the sign which then yields the non strict calculus version See Baumgartner and Furbach 1994a for a discussion of the differences The reader aware of this work will notice that in the present text we define the calculus slightly different This happens in order to conve niently express another calculus variant defined below Note that the restart ME calculus does not assume a special selection function which determines which path is to be ex tended or reduced next Correctness and completeness of this calculus follows immediately from a result in Baumgartner 1994 From the definition of the inference rule extension it follows immediately that this calculus only needs those con trapositives of clauses which contain a positive literal in their heads 2 Computing Answers In this section we introduce the notion of computed answers and we state an answer completeness result for restart ME We assume as given a program P together with one single query Gi A A Gn where the Gis are positive liter als We will often abbreviate such a query as Q where Q stands for the conjunction of Gis The clause set S is the transformation of P U Q into goal normal form In the following definition of computed answer
15. lauses A connection is a pair of literals written as K L which can be made com plementary by an application of a substitution A path is a se quence of literals written as p Ly L Ln is called the leaf of p which is also denoted by leaf p similarly the first element L is also denoted by first p The symbol o denotes the append function for literal sequences In the sequel both path sets and sets of literals are always understood as multisets and usual set notation will be used Multisets of paths are written with caligraphic capital letters From now on we use the notation Aj V VAm Bi A A By as a representation of the clause A V V Am V B V V By Such clauses are called program clauses with head literals A if present and body literals Bi We assume our clause sets to be in goal normal form 1 e there exists only one goal clause a clause containing only negative literals which furthermore does not contain vari ables Without loss of generality this can be achieved by in troducing a new clause goal where goal is a new predi cate symbol and by modifying every purely negative clause B V V By to goal Bj Bn IfC A V VAm Bi A ABy isa clause then its path set Pc is L L Ay Am 7Bi 7Bu The dot product p Q of a path p and a path set Q is defined as poq q Q It can be interpreted as a branching of a path p into the new paths from Q The i
16. nference rule extension from the restart ME calcu lus will be defined in such a way that one is free in selecting any head literal as part of a connection For this we introduce a head selection function Definition 1 1 Head selection Function A head selection function f is a function that maps a clause A V V An amp Bid A Bm with n gt 1 to an atom L Aj An L is called the selected literal of that clause by f The head selection function f is required to be stable under lifting which means that if f selects Ly in the instance of the clause A V V An B A A Bm y for some substitution y then f selects L in Aj V V An amp Bi A A Bm O Note that this head selection function has nothing to do with the selection function from SLD resolution which se lects subgoals This will be discussed later Definition 1 2 Strict Restart Model Elimination Given a set of clauses S and a head selection function The inference rule extension is defined as follows PU p Ai V VAiV V Am amp B14 A Bn R where 1 Ff Ups 1S a path multiset and Ag Vi V AIV V Am amp B A A By is a variable disjoint variant of a clause in S A is the selected literal and 2 leaf p Aj is a connection with MGU and 3 R PU po K Ke Ai Ai 1 Aiyi Am 7Bi Bn o The inference rule reduction is defined as follows PU p ane where Po 1 P U p is a path multiset and
17. oaches introduce new calculi or proof procedures for which efficient implementations still have to be developed For a thorough discussion we refer to Baumgartner and Furbach 1994a Our aim was to modify ME such that it can be used for logic programming in the above sense This gives us the possibility to use existing the orem provers for disjunctive logic programming As a first step towards this goal we introduced in Baumgartner and Furbach 1994a the restart variant of ME and proved its refu tational completeness In this paper we introduce an answer computing mechanism into restart model elimination proofs of all stated theorems can be found in the long version Baum gartner et al 1995 Furthermore we define a variant called ancestry restart ME which allows extended regularity check ing i e loop checking wrt the ordinary restart ME Addi tionally this variant prefers proofs which allow for definite answers For the second aspect namely computing answers we ac commodated our PROTEIN system Baumgartner and Fur bach 1994b for answer computing as described below We demonstrate with some of Smullyan s puzzles Smullyan 1978 that it is much more difficult to compute answers in stead of only to prove unsatisfiability For this we give a com parative study of high performance theorem provers includ ing OTTER SETHEO and our PROTEIN system 1 From Tableau to Restart Model Elimination 1 1 Tableau Model Elimination
18. prove the existence of answers Concerning the first aspect it is important to note that there is a lot of work towards model theoretic semantics of positive disjunctive logic programs and of course there are numer ous proposals for non monotonic extensions However with respect to interpretation i e proof theoretic investigations the situation is not so clear At first glance one might be con vinced that any first order theorem prover can be used for the interpretation of disjunctive logic programs since a program clause A V V Am B A A Bn is a representation of the clause A V V Am V B V V aBn Indeed in Lobo et al 1992 SLI resolution is used as a calculus for disjunctive logic programming From logic programming with Horn clauses however we learn that for a procedural interpretation of program clauses it is crucial that clauses can only be accessed by the literals Aj i e by the head literals Technically this means that only those contrapositives are al lowed to be used which contain a positive literal in the head The approach from Lobo et al 1992 completely ignores this aspect by using SLI resolution which requires all contra positives There are proposals for first order proof calculi using pro gram clauses only in this procedural reading e g Plaisted s problem reduction formats Plaisted 1988 or the nearHorn Prolog family introduced by Loveland and his co workers Loveland 1991 These appr
19. r contains less or equal literals than the given answer All proofs are stated in the long version of this paper Baumgartner et al 1995 3 Definite Answers and Regularity From theorem proving with ME we know that the regularity check is an important means for improving efficiency Regu larity for ordinary ME means that it is never necessary to con struct a tableau where a literal occurs more than once along a path Expressed more semantically it says that it is never nec essary to repeat in a derivation a previously derived subgoal viewing open leaves as subgoals Unfortunately regularity is not compatible to restart ME In this section we will present a variant of restart ME the ancestry restart variant which allows for extended regularity checks This variant is motivated by Loveland s UnH Prolog Loveland and Reed 1992 As an interesting side effect it turns out that this variant of fers considerable benefits with respect to logic programming occasionally one is interested in the question whether a given program with query admits a definite answer i e an answer which is a single conjunction of atoms but not a disjunction Of course in general a non definite program does not always admit a definite answer but some programs do It is the latter class of problems we are interested in now The key idea to the direct computation of definite answers is to restrict the use of the query to one single application in tne
20. refutation Namely at its top 1nen OY denon dennite answers are obtained However such a restriction is incom plete But if restart ME is modified in such a way that every negative literal along a branch not only the topmost literal may be used for the restart step then completeness is recov ered This follows from a more general result which states that we can restrict to globally regular refutations i e no lit eral except the literal used for the restart occurs more than once along a branch Let us now introduce all this more for mally Definition 3 1 Ancestry Restart Model Elimination The calculus an cestry restart ME is the same as strict restart ME Defini tion 1 2 except that the inference rule restart is modified by replacing the condition 3 by the new condition 3 3 L is a negative literal occurring in p In this context L is also called the restart literal The modified rule is called ancestry restart O The term ancestry in the definition is explained by the use of ancestor literals for restart steps Note that any reduction from a positive leaf literal to a negative ancestor literal can be simulated in ancestry restart ME by a restart step followed by a strict reduction step Thus non strictness is built in into ancestry restart ME Note that the ancestry restart rule includes the restart rule since the first literal can be used for the restart as well Clearly in terms of a proof procedure
21. s used exactly once namely at the first extension step of goal The last theorem enables us to enumerate definite answers only by simply restricting the use of goal Q to one exten sion step at the beginning So we have the desirable properties of loop checking by regularity and the computation of definite answers 4 Implementation All variants and refinements of ME discussed so far i e the restart strict and ancestry variants possibly with selection function loop checking by regularity and factorization are implemented in the PROTEIN system Baumgartner and Fur bach 1994b It is a first order theorem prover based on the Prolog technology theorem proving PTTP technique imple mented in ECLiPSe Prolog Since ME is a goal oriented linear and answer complete calculus it is well suited as an interpreter for disjunctive 10gic programming FRKU BUN Taciiitates Computing disjunc tive and definite answers In its newest release their is also a flag which allows us to look for definite answers only 5 Comparative Theorem Prover Study In the sequel we want to tell about our experiences in com puting answers by using theorem provers First of all we had to overcome some technical problems because theorem provers usually do not supply answers besides yes or pos sibly no We will illustrate our experiences with a puzzle example which allows for indefinite and definite answers 5 1 Knights and Knaves
22. the ancestry restart rule induces a larger local search space than the restart rule On the other side refutations may become much shorter In deed this is the rationale for our proof procedure to search the restart literals from the leaf towards the top As a further benefit of this search order note that a definite answer will be enumerated before a non definite answer Now we are going towards an appropriate completeness result wrt definite answers As mentioned above this result shall be a consequence of a more general result concerning a regularity restriction Let us define this notion precisely Definition 3 2 Regularity Let p be path written as follows the As and Bs are atoms p Bi By A 1B Then p is called blockwise regular iff 1 A Z AJ forl lt ij lt n lLiF j positive literals and Regularity wrt 2 BL Bj forl lt l lt nl lt ij lt k iFj larity inside blocks Regu If additionally it holds that 3 Bi 4 BP forl lt l lt m lt n 1 lt i lt k 2 lt j lt kn Global negative regularity By A A B aBR men p 1S Caed globally regular A path Set Is Called DLOCK wise globally regular iff every path in it is blockwise glob ally regular Similarly a derivation is called blockwise glob ally regular iff every of its path sets is blockwise globally regular O Condition 1 states that all positive literals along a path are pairwise different and condition 2 stat
23. to clausal form is straightforward and therefore omitted here It consists of 11 clauses The symbol V denotes exclusive or 1 true isa Q knight Vtrue isa Q knave 2 says P S gt true S true isa P knight 3 a says asked e b says asked not e where e or isa asked knight isa other knight Cyes no 4 true isa asked X V true isa other Y 5 true not C Vtrue C 6 true or A B 4 true A V true B We Can prove the query 1n many diirerent Ways AS a con sequence we get many trivial and hence useless answers The most trivial one a four part disjunction can be obtained in both cases We only need formula 1 and the query in order to infer it But it only says that each of both persons are either knights or knaves In case a if the asked person says yes we can get an indefinite answer consisting of only three disjuncts In the other case b there exists a definite answer It follows a list of these possible answers where X Y is an abbreviation of true isa asked X A true isa other Y 1 knave knave V knave knight V knight knave V knight knight trivial 2 knave knave V knight knave V knight knight indefinite 3 knave knight definite Before turning to our experiments we want to mention some interesting facts Firstly answer completeness requires that we are able to compute the indefinite and definite answer in the respective cases Secondly to der
24. we collect appli cations of the query clause but not applications of negative clauses from the program P Definition 2 1 Answers If Q is a query and 81 9m are substitutions for the variables from Q then Q81 V V Qm is an answer for S An answer Q6 V V Qm is a correct answer if P H V Q6 V V Q m Let now a restart ME refutation of S with goal clause goal and substitution be given Assume that this refutation contains m extension steps with the query i e it contains m times an extension step with the clause goal Qp where p is the renaming substitution of this step Let ci pid dom p Then Qoi V V Qom is a computed answer for S O Theorem 2 2 Lifting Theorem for Restart Model Elimination Let S be a set of ground instances of clauses taken from a clause set S Assume there exists a restart ME derivation D Po P1 P from S with goal clause Ch S Then there exists a restart ME derivation D Po Pi Pn from S with some goal clause Cg S and substitution o such that P is more general than P A path set P is more general than a path set Q iff for some substitution 6 we have Pd Q Furthermore there exists a substitution 6 such that P is obtained from P _ by an extension step with clause C S if and only if P is obtained from P _ by an extension step with a clause C S such that Cpo C where p is the renaming substitution applied in that extension step
Download Pdf Manuals
Related Search
Related Contents
Graseby MR10 Neonatal Respiration Monitor Handy Pìco Operating Instructions User Manual USB 300 / USB 300C / USB 300U (OEM) Solar Water Heater Owners Guide ICC IC107BC1WH outlet box ET-705C MANUAL Medidor por capacitancia de la serie PROCAP I Instructivo de Critères MPE de l`UE pour le matériel informatique de bureau SP Series User Manual Programming Worksheets Fiches De Programmation Hojas Copyright © All rights reserved.