Do We Need Existential Quantifiers in Logic Programming? Date: 30 Mar 2007 From: Vladimir Lifschitz To: TAG In a recent e-mail, Len Schubert expressed the view that logic programs are a viable alternative to resolution theorem proving for solving textual entailment problems. He said that his own primary interest is in generality, that he would like to find out what representational and reasoning techniques will be needed for comprehensive language understanding and commonsense reasoning, and that none of the techniques used so far in work on recognizing textual entailment quite meet that general challenge. And then he added: In the case of logic programs, I immediately think of examples like "Kofi is a married man" textually entails "Kofi has a wife" (based on the knowledge that every married man has a wife -- and I don't have in mind a "has-a-wife" predicate :-). This is an interesting example! Formalizing it in first-order logic is straightforward: Given fact: Married(Kofi) Background knowledge: Male(Kofi) Married(x) & Male(x) -> exists y Wife(y,x) Consequently: exists y Wife(y,Kofi) What is the counterpart of this use of "exists y" in logic programming? =========== Date: 31 Mar 2007 From: Martin Brain To: Vladimir Lifschitz I'm not sure that it answers your question and it is probably a pragmatic rather than a 'correct' approach, but I'd encode it as: married(kofi). male(kofi). _false :- male(X), married(X), not hasWife(X). hasWife(X) :- wife(Y,X). because I see the conclusion ( "exists y Wife(y,Kofi)" ) as an constraint on the type of world view that is possible, rather than information within the world view. Ofcourse to be able to handle this directly with an LP system, you'd need some way of saying that Y is an unknown domain and then returning results that specify constraints from that domain. =========== Date: 2 Apr 2007 From: Vladimir Lifschitz To: Martin Brain > married(kofi). > male(kofi). > _false :- male(X), married(X), not hasWife(X). > hasWife(X) :- wife(Y,X). This program has no stable models, right? How do we see from it that Kofi has a wife? > Ofcourse to be able to handle this > directly with an LP system, you'd need some way of saying that Y is an > unknown domain and then returning results that specify constraints from > that domain. I'm afraid I don't understand this at all. Please explain. =========== Date: 4 Apr 2007 From: Martin Brain To: Vladimir Lifschitz > This program has no stable models, right? How do we see from it that Kofi > has a wife? I was intending it to be a fragment of a program rather than the complete program. The complete programs would also have rules that could infere wife(Y,X). > > Ofcourse to be able to handle this > > directly with an LP system, you'd need some way of saying that Y is an > > unknown domain and then returning results that specify constraints from > > that domain. > > I'm afraid I don't understand this at all. Please explain. Sorry - I didn't explain myself very well. What I was thinking was that if we wanted to be able to handle the given program (fragment) on it's own then some additional mechanism would have to be added to the solver to supply some non constructive information about the context of the program. In this case, adding a statement saying "wife(Y,X) is not given by any rule, but could potentially be true if needed". Thus rather than returning answer sets it would return answer ste sand constraints on the context information provided. So this fragment returns { married(kofi), male(kofi), hasWife(kofi) } and the constraint "wife(Y,kofi) must be true in the context this fragment is used". Does this help? As I suggested before it's a bit of a hack-ish way of approaching the problem. =========== Date: 4 Apr 2007 From: Vladimir Lifschitz To: Martin Brain > I was intending it to be a fragment of a program rather than the > complete program. The complete programs would also have rules that > could infere wife(Y,X). I see what you are saying. But common sense allows us to conclude that Kofi has a wife from the assumption that Kofi is married even in the absence of such additional information! Schubert's question (and mine) is whether this kind of commonsense reasoning can be simulated in logic programming. =========== Date: 4 Apr 2007 From: Peter CLARK To: Vladimir Lifschitz Um...doesn't one just Skolemize the existential? wife(X,f(X)) :- married(X), male(X). Or are terms not allowed in logic programs? Excuse my total ignorance here! =========== Date: 4 Apr 2007 From: Vladimir Lifschitz To: Peter Clark Yes, terms are allowed in logic programs! Let's replace the corresponding rule in Martin's program by your Skolemized version: married(kofi). male(kofi). wife(X,f(X)) :- married(X), male(X). hasWife(X) :- wife(X,Y). This program has a unique stable model {hasWife(kofi),wife(kofi,f(kofi)),male(kofi),married(kofi)} that indeed contains the expected conclusion hasWife(kofi). I would have said that Skolemization is a completely satisfactory answer to Schubert's question, if not for the fact that sometimes Skolem functions exhibit peculiar behavior when they are used in a logic program along with equality. For instance, add these two rules to the program above: wife(kofi,natasha). :- wife(X,Y1), wife(X,Y2), Y1!=Y2. (The last rule encodes the assumption that a man has at most one wife.) The extended program has no stable models. Isn't this strange? =========== Date: 4 Apr 2007 From: Peter Clark To: Vladimir Lifschitz It looks like logic programming's built-in unique names assumption is getting in the way here. It does make things tricky, if one removes the UNA then it makes the machinery for reasoning a whole lot more complicated! FYI, I should add in KM (our KR language www.cs.utexas.edu/users/mfkb/km) we don't make the UNA for Skolems so this example isn't a problem in that language. But then to get away with the complications this introduces for equality reasoning, KM does some "heuristic" (unsound) unification of entities, i.e., it has some heuristics about when equality can be assumed, even if not provable. (In the below example one could avoid these heuristics by also adding the constraint that a Married-Person has exactly 1 spouse, but in general the heuristics are needed). (Married-Person has (superclasses (Person))) (every Married-Person has (spouse ((a Person)))) ;;; wife(X,Y) -> spouse(X,Y) (wife has (superslots (spouse))) (*Kofi has (instance-of (Married-Person)) (wife (*Natasha))) #| Then: KM> (the spouse of *Kofi) (COMMENT: (*Natasha && _Person1) unified to be *Natasha) (*Natasha) |# =========== Date: 4 Apr 2007 From: Sandeep Chintabathina To: Vladimir Lifschitz >I would have said that Skolemization is a completely satisfactory answer >to Schubert's question, if not for the fact that sometimes Skolem functions >exhibit peculiar behavior when they are used in a logic program along with >equality. For instance, add these two rules to the program above: > > wife(kofi,natasha). > :- wife(X,Y1), wife(X,Y2), Y1!=Y2. > >(The last rule encodes the assumption that a man has at most one wife.) >The extended program has no stable models. Isn't this strange? I do agree that this is strange but the fact that "f(kofi)= natasha" is not captured by the logic program. An alternative would be to provide the logic program with this information. I would redefine my equality relation in this case. Here is an extended version of your program: married(kofi). male(kofi). wife(X,f(X)) :- married(X), male(X). hasWife(X) :- wife(X,Y). wife(kofi,natasha). :- wife(X,Y1), wife(X,Y2), not_equal(Y1,Y2). equal(f(kofi),natasha). equal(natasha,f(kofi)). not_equal(X,Y) :- not equal(X,Y), X!=Y, person(X), person(Y). person(kofi). person(natasha). person(f(kofi)). This program has one stable model: { wife(kofi,natasha) wife(kofi,f(kofi)) hasWife(kofi) male(kofi) married(kofi) person(natasha) person(kofi) person(f(kofi)) not_equal(kofi,natasha) not_equal(natasha,kofi) not_equal(f(kofi),kofi) not_equal(kofi,f(kofi)) equal(f(kofi),natasha) equal(natasha,f(kofi)) } that contains the expected conclusion hasWife(kofi). =========== Date: 4 Apr 2007 From: Peter Clark To: Sandeep Chintabathina sThe practical problem with (at least) Prolog is that a definition of equality which makes the unique names assumption is built in to its unification algorithm. So if you want to redefine equality as you do below, you would also need to write a different Prolog (say) interpreter which would allow (for example) female(natasha) and female(f(kofi)) to successfully unify. =========== Date: 4 Apr 2007 From: Michael Gelfond To: TAG 1. On Sandeep's solution and Pete's comment: Answer set solvers do not use unification. The models are usually computed by a smart grounding process and a (substantially modified) satisfiability algorithm. So, say, Smodels will compute the model of Sandeep's program and give the correct answer. 2. On Vladimir's question: What is the counterpart of this use of "exists y" in logic programming? It depends on what you mean by logic programming. For instance, the following married(kofi). male(kofi). exists y wife(Y,X) :- married(X), male(X). is a program in the language of epistemic specifications from M. Gelfond and H. Przymusinska, "Reasoning in Open Domains", Logic Programming and Nonmonotonic Reasoning, Edited by L Pereira and A. Nerode, pp. 397-413, the MIT press, 1993. M. Gelfond, "Logic Programming and Reasoning with Incomplete Information" Annals of Mathematics and Artificial Intelligence, 12, pp. 89-116 1994. We can forget modal operators introduced there and only look at the subset of the language which consists of rules f :- f1,...,fn, not g1,...not gm where f's and g's are formulas constructed from atoms using conjunction, strong negation, and existential quantifiers. In addition to the usual answer set construction the semantics expands the signature of a program by new (Skolem) constants c1, c2, etc. The program entails exists Y wife(Y,kofi). In the above papers existential quantifiers were used to explicitly express the domain closure assumption, the unique name assumption, to deal with integrity constraints and some other things. I am not sure if all of this can be done in classical logic. (Those interested in details can look at my WEB page or just ask questions) Even though the classical logic solution and the above program look almost identical there are substantial differences between the two. In epistemic specification as in most other LP languages models (answer sets, belief sets, etc) are countable. This makes LP very different from classical logic. So my question is "Do we really need KR languages which allow uncountable models?" =========== Date: 5 Apr 2007 From: Michael Gelfond To: Vladimir Lifschitz below is a description of the treatment of the Len's problem by our question answering system ATM. Ideologically it is similar to that of Peter and Sandeep, but it is longer and possibly more systematic. Please do not take me too seriously here - the system is work in progress and is constantly evolving. ATM start with the text: " John is married" and calls the natural language processing program, LFT, which turn this sentence into so called LFT logic form. In a somewhat simplified format LFT logic form looks like: john(x1) & human(x1) & marry(e1,x1,x2) Intuitively it says that "e1" is an action of the type "marry", that "e1" has two participants, "x1" and "x2", that the name of the first participant is John and that he is human. Intuitively we view x1, x2, etc as "internal names" of the objects of the domain. Each object has the unique internal name assigned to it. There are (possibly defeasible) unique name assumptions for internal names and for proper names. x1 is different from x2 and Michael from John, even though Michael and Misha may serve as names of the object denoted by some internal name "x". The part of our system, called semantic translator, will translate the LFT form into atoms classifying our symbols name(john). internal_name(x1). internal_name(x2). name_of(john,x1). and atoms describing action, e1: action(e1). type(e1,marry). participant(e1,john). participant(e1,x2). human(john). male(john). occurs(e1,0). The fact that John is male comes from background knowldge. Internal name x1 is replaced by the corresponding proper name, John. Constant x2 remains unnamed. In addition to our semantic representation of the story (called ATM logic form) we will also have a short theory of traditional western marriage containing axioms 1. holds(married(X,Y),S2) :- next(S2,S1), occurs(A,S1), type(A,marry), participant(A,X), participant(A,Y), different(X,Y). 2. holds(wife(Y,X),S) :- holds(married(X,Y),S), male(X). 3. -holds(wife(X2,Y),S) :- holds(wife(X1,Y),S), different(X1,X2). plus general theory of actions including inertia, etc.. (standard and mostly skipped), and general axioms defining "different". The definition of "different" is tentative and makes use of the distinction between proper and internal names. different(X,Y) :- internal_name(X), internal_name(Y), X != Y, not -different(X,Y). different(X,Y) :- name(X), name(Y), X != Y, not -different(X,Y). different(X,Y) :- internal_name(X), internal_name(Z), name(Y), name_of(Y,Z), X != Z, not -different(X,Y). different(X,Y) :- different(Y,X). Let us denote the resulting program by P. The question, "Does John have a wife?" can be translated into something like: answer(yes) :- holds(wife(X,john),1). The program P has unique answer set containing holds(wife(x2,john),1) and answer(yes). Hence John has a wife. If we expand the program by name(mary). (which of course can be there in some ontology of names), and 4. holds(wife(mary,john),1). we will have no contradiction since we cannot prove that x2 and Mary are different. John still has a wife. This is of course just a sketch. We probably need to add some axioms refining the meaning of name_of, etc. But I hope it will give you a flavor of what we are doing. Comments (from everyone) are of course greatly appreciated. =========== Date: 5 Apr 2007 From: Yuliya Lierler To: Michael Gelfond > ATM start with the text: " John is married" > and calls the natural language processing program, LFT, > which turn this sentence into so called LFT logic form. > In a somewhat simplified format LFT logic form looks like: > > john(x1) & human(x1) & marry(e1,x1,x2) > > Intuitively it says that "e1" is an action of the type "marry", > that "e1" has two participants, "x1" and "x2", that the name > of the first participant is John and that he is human. > Intuitively we view x1, x2, etc as "internal names" of the > objects of the domain. Each object has the unique internal > name assigned to it. Very interesting. It seems that here the problem of "existential quantifier" disappears during the phase of translating NL input into corresponding semantic representation. In your example the counterpart for word "married" is a predicate "marry(e1,x1,x2)" that (1) represents the action that leads one to being married and (2) introduces a second participant of an action, in this case -- x2, that given the rules you provided below will be inferred to be wife of John. It seems that in Vladimir's question he considered an alternative semantic representation to "John is married" as "john(x1) & human(x1) & married(x1)". > If we expand the program by > > name(mary). (which of course can be there in some ontology of names), and > > 4. holds(wife(mary,john),1). > > we will have no contradiction since we cannot > prove that x2 and Mary are different. John still has a wife. > What if we expand the program by: name(mary). name(lucy). ? what would the query 5. holds(wife(mary,john),1). yield? Another comment that I have deals with Sandeep's program: It seems that similarly as given that X is married we would like to infer that he has a wife, given that X has a wife we would like to infer that X is married. We can extend a program given by Sandeep by adding the following rule: married(X):-hasWife(X). Note that by adding such rule program becomes nontight. In this case using classical logic to represent such knowledge would be not a straight forward task. =========== Date: 5 Apr 2007 From: Vladimir Lifschitz To: Michael Gelfond > 2. On Vladimir's question: What is the counterpart of this use of > "exists y" in logic programming? > > It depends on what you mean by logic programming. > For instance, the following > > married(kofi). > male(kofi). > exists y wife(Y,X) :- > married(X), > male(X). > > is a program in the language of epistemic specifications from > > M. Gelfond and H. Przymusinska, "Reasoning in Open Domains", > Logic Programming and Nonmonotonic Reasoning, Edited by L Pereira > and A. Nerode, pp. 397-413, the MIT press, 1993. > M. Gelfond, "Logic Programming and Reasoning with Incomplete > Information" > Annals of Mathematics and Artificial Intelligence, 12, pp. 89-116 1994. Yes, and also you can write such rules in the language proposed in the paper P. Ferraris, J. Lee and V. Lifschitz, "A new perspective on stable models", in Proceedings of IJCAI-07, 2007. So I was thinking -- perhaps languages of this kind, with explicit existential quantifiers, can provide solutions that will be particularly simple and natural from the user's perspective; formalizations like those described by Pete and Sandeep and yourself may turn out to be provably equivalent to those solutions. Perhaps we can think of them as "lower level" reformulations important because they are more directly implementable. This would be similar to what we do in resolution theorem proving: quantifiers can be used in the axioms and in the conjecture, but they are eliminated in favor of Skolem constant in the process of converting the problem to clausal form. =========== Date: 6 Apr 2007 From Michael Gelfond To: Vladimir Lifschitz > Yes, and also you can write such rules in the language proposed in the > paper > > P. Ferraris, J. Lee and V. Lifschitz, "A new perspective on stable > models", in Proceedings of IJCAI-07, 2007. > You are right. And this raises a number of questions I believe to be important, e.g. What is the relationship between this new language and the older language of epistemic specifications (ES)? (We certainly can compare their subsets). Can the new language express domain closure assumption and other language constructs expressible in ES? Can it express more? (For instance I do not remember if models of the new language can be uncountable) > So I was thinking -- perhaps languages of this kind, with explicit > existential quantifiers, can provide solutions that will be > particularly > simple and natural from the user's perspective; formalizations like > those > described by Pete and Sandeep and yourself may turn out to be provably > equivalent to those solutions. Perhaps we can think of them as "lower > level" reformulations important because they are more directly > implementable. This would be similar to what we do in resolution > theorem > proving: quantifiers can be used in the axioms and in the > conjecture, but > they are eliminated in favor of Skolem constant in the process of > converting the problem to clausal form. I agree. But I also think that it is essential to spend some time understanding and comparing semantics of "exists X" given by different languages, and analyzing methodology of their use. =========== Date: 6 Apr 2007 From: Vladimir Lifschitz To: Michael Gelfond > And this raises a number of questions I believe to be important, e.g. > What is the relationship between this new language and the older > language of epistemic specifications (ES)? Right. One more semantics of quantifiers in logic programs that should be compared with the others is defined in Section 7 of the paper Fangzhen Lin and Yi Zhou, "From answer set logic programming to circumscription via logic of GK", in Proceedings of IJCAI-07, 2007. It is "almost equivalent" to the new semantics by Ferraris et al. At the same time, it is similar in a way to the ES approach: it involves replacing quantifiers by finite conjunctions and disjunctions over "new" object constants not occurring in the program. > (For instance I do not remember if models of the new language can be > uncountable) Yes, although we have not yet thought of using this possibility in applications to KR. Our definition of a stable model, like McCarthy's definition of circumscription, can be thought of as a generalization of the semantics of classical logic. If we conjoin a first-order sentence with the "choice rules" forall x (P(x) V -P(x)) for all predicate constants P occurring in it then the difference between stable models and arbitrary models will disappear. Going back to your previous message, > ATM start with the text: " John is married" > and calls the natural language processing program, LFT, > which turn this sentence into so called LFT logic form. > In a somewhat simplified format LFT logic form looks like: > > john(x1) & human(x1) & marry(e1,x1,x2) > > Intuitively it says that "e1" is an action of the type "marry", > that "e1" has two participants, "x1" and "x2", that the name > of the first participant is John and that he is human. It's curious that the LFT logic form of "John is married" involves the action "marry". What is the LFT logic form of "John is shy"? =========== Date: 6 Apr 2007 From: Marcello Balduccini To: Vladimir Lifschitz > It's curious that the LFT logic form of "John is married" involves > the action "marry". What is the LFT logic form of "John is shy"? Yes, quite peculiar. The LFT system sometimes does not distinguish well between copula and passive form. I am pretty picky about grammar, so that tends to get annoying. On the bright side, in practice it does not cause problems with the examples we use it on. I can't get the logic form of "John is shy" right now, because the server appears to be down. I believe however that it will look something like: john(x1) & shy(x1) (verb "to be" is skipped when identified as copula) =========== Date: 6 Apr 2007 From: Peter Clark To: Marcello Balduccini > Yes, quite peculiar. The LFT system sometimes does not distinguish well > between copula and passive form.... Well, it's not *that* peculiar -- it's a valid (albeit unusual) alternative reading of the sentence. In general, the adjective/passive distinction in NLP remains as a hugely difficult disambiguation problem. =========== Date: 6 Apr 2007 From: Chitta Baral To: Michael Gelfond > But I also think that it is essential to spend some time understanding > and comparing semantics of "exists X" given by different languages, > and analyzing methodology of their use. The above is a good idea and I was starting to do that yesterday. In this regard, some of the older discussions in the literature on this issue is mentioned in the book "Knowledge Representation, reasoning and declarative problem solving" in the pages: 471-474 (9.5), 492-293 (references), 314-316 (6.6.2) Just thought it may come in handy. =========== Date: 6 Apr 2007 From: Joohyung Lee To: Vladimir Lifschitz > So I was thinking -- perhaps languages of this kind, with explicit > existential quantifiers, can provide solutions that will be particularly > simple and natural from the user's perspective; formalizations like those > described by Pete and Sandeep and yourself may turn out to be provably > equivalent to those solutions. Perhaps we can think of them as "lower > level" reformulations important because they are more directly > implementable. This would be similar to what we do in resolution theorem > proving: quantifiers can be used in the axioms and in the conjecture, but > they are eliminated in favor of Skolem constant in the process of > converting the problem to clausal form. I agree with the idea. Indeed, a first-order sentence under the new definition of stable model semantics can be turned into a prenex normal form whose matrix is in the form of a logic program. Lee and Palla, "Yet another proof of the strong equivalence between propositional theories and logic programs", Section 4. (Unpublished draft available at http://peace.eas.asu.edu/joolee/papers/f2lp.ps . ) More understanding of existential quantifiers left in the prenex normal form may tell us how to view the new language as a high level formalism for logic programs. =========== Date: 6 Apr 2007 From: Gerald Pfeifer To: Vladimir Lifschitz > I see what you are saying. But common sense allows us to conclude > that Kofi has a wife from the assumption that Kofi is married even > in the absence of such additional information! Only if we exclude same sex marriage (which is legal in several countries). In this case, also _false :- male(X), married(X), not hasWife(X). will be too strict. The point I am trying to make here is not one focusing on this specific case, but more towards the fact that more general representations may be more resilient in such situations. (hasWife(_) here does strike me as a bit unnatural a predicate.) =========== Date: 6 Apr 2007 From: Vladimir Lifschitz To: Gerald Pfeifer > Only if we exclude same sex marriage (which is legal in several > countries). In a same sex marriage certificate, are the spouses identified as husband and wife, or just as spouses? > hasWife(_) here does strike me as a bit unnatural a predicate Right. I would prefer exists X wife(_,X). And who knows, maybe answer set solvers of the future will allow us to use this syntax. =========== Date: 6 Apr 2007 From: Ricardo Morales To: TAG > In the case of logic programs, I immediately think of examples > like "Kofi is a married man" textually entails "Kofi has a wife" > (based on the knowledge that every married man has a wife -- and > I don't have in mind a "has-a-wife" predicate :-). The following is another perspective in how to represent such knowledge: person(kofi). person(natasha). person(john). person(mary). person(martin). person(claudia). person(peter). person(susan). male(kofi; john; martin; peter). female(natasha; mary; yuliya; susan). married(kofi). 1{wife(X,Y) : female(Y)}1 :- married(X), male(X). The Last rule encodes that as Kofi is married, it most have exactly one wife (who is female). This program has 4 models: {married(kofi), wife(kofi,natasha)} {married(kofi), wife(kofi,mary)} {married(kofi), wife(kofi,claudia)} {married(kofi), wife(kofi,susan)} If we add the fact 'wife(kofy,natasha)' only the first model remains (as expected). Of course, this works only because we have names for every object of the domain. The way I see the problem, it is not only about existential quantifiers, but also about how to reason with large/infinite domains. I imagine an answer-set solver that could answer queries about programs with infinite models. (without having to evaluate the whole model, of course). =========== Date: 6 Apr 2007 From: Vladimir Lifschitz To: Ricardo Morales > The way I see the problem, it is not only about existential quantifiers, > but also about how to reason with large/infinite domains. More importantly, I would say, how to reason when the domain is unknown. Your formalization assumes exactly 4 males and exactly 4 females. What if we only know that each number is between 1 and 10? We'd like a single formalization, not separate formalizations for 100 possible cases. =========== Date: 6 Apr 2007 From: Chitta Baral To: Vladimir Lifschitz I was reading your IJCAI 07 paper yesterday. I was confused by the use of implication as an explicit connective and the absence of classical negation as an explicit connective. Can we still call it "classical logic". I understand that you can represent ~F as F -> bottom. I was wondering if one can use traditional classical logic with only "or", "and", and "negation" connectives, with the usual meaning of implication, and then define SM[F] (as you do now in Section 2.3) on such traditional classical logic formulas F. =========== Date: 6 Apr 2007 From Vladimir Lifschitz To: Chitta Baral Actually it's negation as failure, not classical (strong) negation, that we identify with F->bottom. In our IJCAI-07 paper strong negation is not present even implicitly. But it's easy to add it on top the new definition; see Sec. 3.9 of the paper Paolo Ferraris and Vladimir Lifschitz, "Mathematical foundations of answer set programming," in: We Will Show Them! Essays in Honour of Dov Gabbay, Vol. 1, 2005, pp. 615-664 (http://www.cs.utexas.edu/users/vl/papers/mfasp.ps). > I was wondering if one can use traditional classical logic with only > "or", "and", and "negation" connectives, with the usual meaning of > implication, and then define SM[F] (as you do now in Section 2.3) > on such traditional classical logic formulas F. If by the "usual meaning of implication" you mean treating F->G as shorthand for -F V G then this will not work: these formulas are not strongly equivalent. In logic programming notation, p <- q is not strongly equivalent to the disjunctive rule p ; not q. =========== Date: 6 Apr 2007 From Vladimir Lifschitz To: Chitta Baral Actually it's negation as failure, not classical (strong) negation, that we identify with F->bottom. In our IJCAI-07 paper strong negation is not present even implicitly. But it's easy to add it on top the new definition; see Sec. 3.9 of the paper Paolo Ferraris and Vladimir Lifschitz, "Mathematical foundations of answer set programming," in: We Will Show Them! Essays in Honour of Dov Gabbay, Vol. 1, 2005, pp. 615-664 (http://www.cs.utexas.edu/users/vl/papers/mfasp.ps). > I was wondering if one can use traditional classical logic with only > "or", "and", and "negation" connectives, with the usual meaning of > implication, and then define SM[F] (as you do now in Section 2.3) > on such traditional classical logic formulas F. If by the "usual meaning of implication" you mean treating F->G as shorthand for -F V G then this will not work: these formulas are not strongly equivalent. In logic programming notation, p <- q is not strongly equivalent to the disjunctive rule p ; not q. =========== Date: 6 Apr 2007 From: Chitta Baral To: Vladimir Lifschitz Based on your clarification, it seems to me the language in the IJCAI'07 paper has some features, connectives and assumptions from logic programming and some from traditional classical logic. From logic programming it has: the implication connective, the negation as failure connective From traditional classical logic it has: quantifiers, use of models instead of Herbrand models (as a result no domain closure assumptions), no unique name assumptions Its a nice language and I need to think about it more. =========== Date: 11 Apr 2007 From: Marcello Balduccini To: Yuliya Lierler > What if we expand the program by: > name(mary). > name(lucy). ? > > what would the query > > 5. holds(wife(mary,john),1). > > yield? As far as I can see, adding name(lucy) to Michael's program does not affect the answer to the original question. The program still entails answer(yes) holds(wife(mary,john),1) The program now also entails -holds(wife(lucy,john),1) Is that what you were expecting? =========== Date: 20 Apr 2007 From: Yuliya Lierler To: Marcello Balduccini Now I understand Michael's solution better. I understood his previous message a little different. Let me explain what I find slightly unnatural in "Michael's elaboration (mg2.pl)" solution. Smodels produces one answer set for mg2.pl: Stable Model: name_of(john,x1) answer(yes) holds(wife(mary,john),1) holds(married(john,x2),1) holds(married(x2,john),1) holds(wife(x2,john),1) -holds(wife(john,john),1) -holds(wife(x1,john),1) That we can read as follows: holds(wife(mary,john),1) -- John's wife is Mary holds(married(john,x2),1) -- John is married to someone x2 holds(wife(x2,john),1) -- John's wife is someone x2. First it seems natural that if we know that "John's wife is Mary" then we can conclude that "John is married to Mary". We can easily do it by adding the following rule to Michael's program: holds(married(X,Y),S) :- holds(wife(Y,X),S), male(X). Resulting program yields one answer set: Stable Model: name_of(john,x1) answer(yes) holds(married(john,mary),1) holds(wife(mary,john),1) holds(married(john,x2),1) holds(wife(x2,john),1) holds(married(x2,john),1) -holds(wife(x1,john),1) -holds(wife(john,john),1) We can read it as follows: holds(married(john,mary),1) -- John is married to Mary holds(wife(mary,john),1) -- John's wife is Mary holds(married(john,x2),1) -- John is married to someone x2 holds(wife(x2,john),1) -- John's wife is someone x2. Looking at this solution it seems strange that x2 and Mary are not related to each other as for instance John is related to x1 by name_of(john,x1). (This is related to already discussed equality issue). To fix this we first need to add the following rule that states unless "internal_name" and "name" are different then "name" is a name_of "internal_name": name_of(Y,X):- name(Y), internal_name(X), not different(X,Y). We also need a rule about the names that states if X is different from Y and X is not different from Z, then Y is different from Z. different(Y,Z) :- different(X,Y), not different(X,Z) Also we need the constraint stating that it is impossible that "name" which is name_of "internal_name" are different: :-name_of(X,Y), different(X,Y), name(X), internal_name(Y). The resulting program's answer: Stable Model: name_of(mary,x2) name_of(john,x1) answer(yes) holds(wife(mary,john),1) holds(wife(x2,john),1) holds(married(john,mary),1) holds(married(john,x2),1) holds(married(x2,john),1) -holds(wife(john,john),1) -holds(wife(x1,john),1) It contains predicates name_of(mary,x2), that identifies Mary with x2. Now consider extending the program with the fact name(lucy). New program has one answer set, that states the same facts as previous answer set plus it says that Lucy is different from x1, x2, Mary, and John. The program that I described last is attached to this message. What do you think about new elaborations? If I understand correctly internal_names x1 and x2 stand for what is called extensions. From Wikipedia: "The extension of a general term like "dog" is just all the dogs that are out there; the extension is what the word can be used to refer to." So we can read predicate name_of(mary, x1) as x1 is an extension of proper name Mary. It seems we are adopting the view that there is a name of an object and there is its extension by having name and internal_name in the formalization. If we consider this point is it proper to translate "Mary is a wife of John" as a predicate wife(mary,john)? Shall the translation look differently: wife(x1,x2). name_of(mary,x1). name_of(john,x2). ?