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). ?