The Wolkswagen Domain: Discussion, Part 2
Date: Thu, 9 Sep 1999
From: Esra Erdem and Vladimir Lifschitz
To: Monica Nogueira
> Some questions still remain regarding Esra message. She writes:
>
> 1.
> > We can introduce a new predicate kind/2 and define it by
> >
> > kind(VWR,avwRabbit) <- true.
> > kind(T,atoyota) <- true.
> >
>
> Do we need to use different symbols for sorts and classes?
> Meaning, can we use "toyota" instead of "atoyota", "vwRabbit"
> instead of "avwRabbit", etc?
> In Prolog we can do that which allows to avoid duplicate symbols.
Yes, we have to use different symbols for sorts and classes in the
current version of CCALC.
>
> 2.
> > If we remove CWA then we add
> >
> > -kind(C1,CL) <- not kind(C1,CL).
>
> Isn't this still CWA? It says that for any car C1 and class CL,
> C1 is not of kind CL unless proven otherwise.
You are right, what we said about removing the CWA made little sense.
We take it back.
> 3.
> > - if we declare Mary's car to be just "a car," and ask what kind
> > of car she has, we get the following answer:
> >
> > | ?- query.
> > enter facts (then ctrl-d)
> > |: ^D
> > enter goals (then ctrl-d)
> > |: kind(marysCar,CL).
> > |: ^D
> > calling sato...
> > run time (seconds) 0.06
> > Counterexample: kind(dicksCar,avwRabbit) kind(mikesCar,atoyota)
> > kind(tomsCar,avwRabbit)
> > no
>
>
> If we ask the ground query "Is Mary's car a Toyota?", what would
> be the Ccalc answer? We also know that Dick's car is a vwRabbit.
> What would Ccalc answer if we ask the ground query "Is Dick's car
> a Toyota?"
CCALC will say NO to all of the above questions.
> Since all we know is that Mary has a car, we don't expect an YES.
> If the answer is NO, does it mean that Mary's car is not a Toyota
> or does it mean "UNKNOWN"? Do we get different answers for those
> two questions, or in other words can we distinguish between NO
> and UNKNOWN? (That is what we really mean by "removing CWA".)
CCALC will treat both in the same way. In order to distinguish between
the two, we need to modify our formalization as shown below. In the new
formalization, "vw", "vwRabbit" and "toyota" are not treated as sorts.
Instead, we make them constants and refer to them in the program using
the "kind" predicate, similar to your "isa".
It seems that the CWA is "built in" the CCALC sort mechanism. This is
the price that we have to pay for the convenience of sorted variables.
We shouldn't introduce a sort unless we are prepared to apply the CWA
to it.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Car problem introduced by Michael Gelfond and Monica Nogueira
% Car domain description
% A VW Rabbit is a VW. (1)
% Tom's car is a VW Rabbit. (2)
% Dick's car is a VW Rabbit. (3)
% A VW has an electrical system. (4)
% Part of the electrical system is an alternator. (5)
% The alternator is defective on every VW. (6)
:- op(600,fx,not).
:- macros
not -(#1) -> (#1);
not (#1) -> -(#1).
:- sorts (object >> (car;
electricSystem;
alternator;
airCondSystem));
class.
:- variables
X, Y, Z :: object;
C1 :: car;
CL, CL1 :: class;
AC :: airCondSystem;
ES :: electricSystem;
Alt :: alternator.
:- constants
marysCar,
mikesCar,
dicksCar,
annsCar,
tomsCar ::car;
toyota, vwRabbit, vw :: class;
es(car) :: electricSystem; % es: car -> electricSystem
alt(car) :: alternator; % alt: car -> alternator
ac(car) :: airCondSystem; % ac: car -> airCondSystem
part0(object,object) :: atomicFormula;
part(object,object) :: atomicFormula;
partsOK(object) :: atomicFormula;
isWrong(object,object) :: atomicFormula;
defective(object) :: atomicFormula;
kind(car,class) :: atomicFormula.
% part(X,Y) iff X is a part of Y.
% part0(X,Y) iff X is an immediate part of Y.
% partsOK(X) iff X does not have any defective parts.
% isWrong(X,Y) iff X is a minimal defective part of Y.
% defective(X) iff X is defective.
% kind(C1,CL) iff C1 is a CL.
% part/2 describes the transitive closure of part0/2
% no need to add the irreflexivity of part/2 since part0/2 is acyclic
part(X,Z) <- part0(X,Z).
part(X,Z) <- part0(X,Y), part(Y,Z).
% X is not a part of Y by default
-part(X,Y) <- not part(X,Y).
% If X is a minimal part of Y that is defective, then X is what is wrong
% with Y.
isWrong(X,Y) <- part(X,Y), defective(X), partsOK(X).
% Nothing is wrong with Y by default.
-isWrong(X,Y) <- not isWrong(X,Y).
% If some part X of Z is defective then parts of Z are not OK.
-partsOK(Z) <- part(X,Z), defective(X).
% None of the parts of X are defective by default.
partsOK(X) <- not -partsOK(X).
% If some part Z of X is defective then X is defective as well.
defective(X) <- part(Z,X), defective(Z).
% X is not defective by default.
-defective(X) <- not defective(X).
% Every VW has an ES (describes (4))
part0(es(C1),C1) <- kind(C1,vw).
% Every car has an AC
part0(ac(C1),C1) <- true.
% The alternator of a vw is a part of the ES of that vw (describes (5))
part0(alt(C1),es(C1)) <- kind(C1,vw).
% X is not an immediate part of Y by default
-part0(X,Y) <- not part0(X,Y).
% Every vw has a defective alternator (describes (6))
defective(alt(C1)) <- kind(C1,vw).
% A vwRabbit is a vw. (describes (1))
kind(C1, vw) <- kind(C1, vwRabbit).
% A car is of some kind or not.
-kind(C1,CL) <- not kind(C1,CL).
kind(C1,CL) <- not -kind(C1,CL).
kind(mikesCar, toyota) <- true.
kind(tomsCar, vwRabbit) <- true. % (describes (2))
kind(dicksCar, vwRabbit) <- true. % (describes (3))
kind(annsCar, vw) <- true.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Here are some examples:
| ?- show.
enter specs (then ctrl-d)
|: kind(C1,CL).
|: ^D
yes
1. We declare annsCar to be a car, and define it as a vw. However,
we don't know whether annsCar is a vwRabbit or not.
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: kind(annsCar,vwRabbit).
|: ^D
calling sato...
run time (seconds) 0.24
Counterexample: kind(annsCar,vw) kind(dicksCar,vw)
kind(dicksCar,vwRabbit) kind(mikesCar,toyota) kind(tomsCar,vw)
kind(tomsCar,vwRabbit)
no
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: -kind(annsCar,vwRabbit).
|: ^D
calling sato...
run time (seconds) 0.24
Counterexample: kind(annsCar,vw) kind(annsCar,vwRabbit)
kind(dicksCar,vw) kind(dicksCar,vwRabbit) kind(mikesCar,toyota)
kind(tomsCar,vw) kind(tomsCar,vwRabbit)
no
2. We declare marysCar to be a car, but we don't know what kind of car
it is.
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: kind(marysCar,toyota).
|: ^D
calling sato...
run time (seconds) 0.24
Counterexample: kind(annsCar,vw) kind(dicksCar,vw)
kind(dicksCar,vwRabbit) kind(mikesCar,toyota) kind(tomsCar,vw)
kind(tomsCar,vwRabbit)
no
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: -kind(marysCar,toyota).
|: ^D
calling sato...
run time (seconds) 0.22
Counterexample: kind(annsCar,vw) kind(dicksCar,vw)
kind(dicksCar,vwRabbit) kind(marysCar,toyota) kind(mikesCar,toyota)
kind(tomsCar,vw) kind(tomsCar,vwRabbit)
no
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: kind(marysCar,vw).
|: ^D
calling sato...
run time (seconds) 0.23
Counterexample: kind(annsCar,vw) kind(dicksCar,vw)
kind(dicksCar,vwRabbit) kind(mikesCar,toyota) kind(tomsCar,vw)
kind(tomsCar,vwRabbit)
no
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: -kind(marysCar,vw).
|: ^D
calling sato...
run time (seconds) 0.24
Counterexample: kind(annsCar,vw) kind(dicksCar,vw)
kind(dicksCar,vwRabbit) kind(marysCar,vw) kind(mikesCar,toyota)
kind(tomsCar,vw) kind(tomsCar,vwRabbit)
no
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: kind(marysCar,vwRabbit).
|: ^D
calling sato...
run time (seconds) 0.22
Counterexample: kind(annsCar,vw) kind(dicksCar,vw)
kind(dicksCar,vwRabbit) kind(mikesCar,toyota) kind(tomsCar,vw)
kind(tomsCar,vwRabbit)
no
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: -kind(marysCar,vwRabbit).
|: ^D
calling sato...
run time (seconds) 0.23
Counterexample: kind(annsCar,vw) kind(dicksCar,vw)
kind(dicksCar,vwRabbit) kind(marysCar,vw) kind(marysCar,vwRabbit)
kind(mikesCar,toyota) kind(tomsCar,vw) kind(tomsCar,vwRabbit)
no
3. We declare dicksCar as a car and define it as a vwRabbit.
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: kind(dicksCar,vwRabbit).
|: ^D
calling sato...
run time (seconds) 0.01
yes
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: kind(dicksCar,vw).
|: ^D
calling sato...
run time (seconds) 0.03
yes
| ?- query.
enter facts (then ctrl-d)
|: ^D
enter goals (then ctrl-d)
|: kind(dicksCar,toyota).
|: ^D
calling sato...
run time (seconds) 0.22
Counterexample: kind(annsCar,vw) kind(dicksCar,vw)
kind(dicksCar,vwRabbit) kind(mikesCar,toyota) kind(tomsCar,vw)
kind(tomsCar,vwRabbit)
no
=============
Date: Thu, 23 Sep 1999
From: Vladimir Lifschitz
To: Michael Gelfond
You asked me a while ago what I knew about the relationship between two
kinds of knowledge representation--our logic programming approach on the
one hand, and frame-based systems, such as the one created by Bruce
Porter's group here at UT Austin, on the other. My answer was, "I am
not sure."
Now I do have something to say on this subject. Please have a look at
the note entitled "Translating from CCALC into KM: An Example" available
at http://www.cs.utexas.edu/tag/km.ps . It contains a line-by-line
translation of Esra Erdem's logic programming formalization of your
Volkswagen example into Bruce's system KM, with a few comments. The
group of authors includes Bruce, Pete Clark (who is an expert on KM also),
Joohyung Lee (a student who took Bruce's class recently and did a lot to
help me understand KM) and myself. All of us are on the TAG mailing list.
=============
Date: Fri, 24 Sep 1999
From: Michael Gelfond
To: Esra Erdem and Vladimir Lifschitz
Esra's last message clarified the situation for us. Of course the
problem, even though interesting in itself, was meant to be a preliminary for
the next step - removing CWA, adding defaults, and attaching it to
a dynamic domain. Hopefully, we'll do it some day. Some hierarchy like
this should play a role in a complete solution of the ZOO problem.
We just started to read the KM solution. We are very happy
it is available, but it would help greatly if you could refer
us to some papers which define syntax and (not necessarily formal)
semantics of the language.
=============
Date: Mon, 27 Sep 1999
From: Peter Clark
To: Michael Gelfond
The KM User Manual is at http://www.cs.utexas.edu/users/mfkb/km.html,
which gives the syntax and semantics for KM.
=============
Date: Mon, 27 Sep 1999
From: Bruce Porter
To: Michael Gelfond
Thanks for your interest in the KM language. For a brief introduction to KM,
please see:
http://www.cs.utexas.edu/users/mfkb/km.html
then click on "users manual", the 4th bullet in the list of manuals.
For a quick overview of the language, I recommend that you review
these sections: 1.3, 3-5, 7, 9, 10, 12.1.