The Wolkswagen Domain: Discussion, Part 1
Date: Tue, 9 Feb 1999
From: Michael Gelfond and Monica Nogueira
To: TAG
We are trying to better understand a
formalization of the following problem:
Represent the following statements in LP.
A VW Rabbit is a VW.
Tom's car is a VW Rabbit.
Dick's car is a VW Rabbit.
A VW has an electrical system.
Part of the electrical system is an alternator.
The alternator is defective on every VW.
The problem is taken from the book "Artificial Intelligence
Through Prolog" by Neil C. Rowe.
We are interested to see and compare different formalizations
of this problem.
Later we would like to expand this information by allowing
actions like "replace alternator", etc.
============
Date: Wed, 17 Feb 1999
From: Ale Provetti
To: TAG
One approach I'd take in formalizing Michael and Monica's example is
to use a logical version of semantic networks.
Let us just look at the formalization of the example, written in Prolog.
I use function symbol `:' to build names of components of individual instances.
type(car).
type(vw).
type(vw-rabbit).
is_a(vw,car).
is_a(vw-rabbit,vw). /* plus write default inheritance for predicate is_a */
/* representing individual instances */
instance(i1).
is_a(i1,vw-rabbit).
belongs(i1,tom).
instance(i2).
is_a(i2,vw-rabbit).
belongs(i2,dick).
/* describing parts */
type(elect-sys).
type(alternator).
part_of(elect-sys,vw).
part_of(alternator,elect-sys). /* plus write default inheritance for part_of */
/* parts of individual instances are instances too */
instance(P:I) :- instance(I), part_of(P,I).
/* Now I can write the axiom about defective VW alternators */
feature(alternator:I,defective) :- instance(I), is_a(I,vw), part_of(alternator,I).
What I like of this formalization is:
i) it makes a clear distinction between actual objects in the world, e.g. dick's
car, tom's car alternator.. and categories of objects, e.g., VWs, alternators..
ii) it makes it clear for which predicates default inheritance, and its exceptions,
are needed;
iii) there is an incremental description of objects, so that adding information
about an instance can be captured by adding just a fact concerning the
instance itself.
For instance, asserting that Tom's car is red is captured by adding fact
color(i1,red).
=================
Date: Wed, 17 Feb 1999
From: Esra Erdem
To: TAG
Here is a representation of the car domain in C (presentable to CCALC).
It is a little bit different from what is asked for because an action
replaceAlternator/2 is included. A planning problem within this domain is
also added below.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File car-domain-C
% A VW Rabbit is a VW.
% Tom's car is a VW Rabbit.
% Dick's car is a VW Rabbit.
% A VW has an electrical system.
% Part of the electrical system is an alternator.
% The alternator is defective on every VW.
:- macros maxtime -> 2.
:- include 'C'; 'car-pb-C'. % car-pb-C contains a sample problem
:- sorts vw >> vwRabbit; electricSystem; alternator.
:- variables
VW1, VW2 :: vw;
ES1, ES2 :: electricSystem;
Alt, Alt1, Alt2 :: alternator;
A,A1 :: action.
:- constants
dicksCar, tomsCar :: vwRabbit;
e1,e2 :: electricSystem;
a1,a2,a3,a4 :: alternator;
has_VW_es(vw,electricSystem) :: inertialFluent;
has_VW_alt(vw,alternator) :: inertialFluent;
has_es_alt(electricSystem, alternator) :: inertialFluent;
has_non_def_alt(vw) :: inertialFluent;
defective(alternator) :: inertialFluent;
replaceAlternator(electricSystem,alternator) :: action.
% concurrent actions are not allowed
nonexecutable A && A1 if -(A=A1).
% replaces the alternator of an electric system ES1 with an
% alternator Alt
replaceAlternator(ES1, Alt) causes has_es_alt(ES1, Alt).
% you cannot replace the alternators of two different ESs with the same
% alternator.
nonexecutable replaceAlternator(ES1, Alt) && replaceAlternator(ES2, Alt)
if -(ES1 = ES2).
% you cannot replace the alternator of an ES with one already installed
% at some ES.
nonexecutable replaceAlternator(ES1, Alt) if has_es_alt(ES2,Alt).
caused has_VW_alt(VW1,Alt1) if has_VW_es(VW1,ES1) && has_es_alt(ES1,Alt1).
caused has_non_def_alt(VW1) if has_VW_alt(VW1,Alt1) && -defective(Alt1).
caused -has_non_def_alt(VW1) if has_VW_alt(VW1,Alt1) && defective(Alt1).
caused -has_VW_alt(VW1,Alt1) if has_VW_alt(VW1,Alt2) && -(Alt1 = Alt2).
caused -has_VW_es(VW1,ES1) if has_VW_es(VW1,ES2) && -(ES1 = ES2).
caused -has_es_alt(ES1,Alt1) if has_es_alt(ES1,Alt2) && -(Alt1 = Alt2).
% Every VW has an ES and every ES has an Alt
always (\/ES1: (has_VW_es(VW1,ES1) && (/\ES2: (has_VW_es(VW1,ES2) <->
(ES1 = ES2))))).
always (\/Alt1: (has_es_alt(ES1,Alt1) && (/\Alt2: (has_es_alt(ES1,Alt2) <->
(Alt1 = Alt2))))).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File car-pb-C
:- plan
facts ::
init -defective(a1),
init -defective(a2),
init has_VW_es(dicksCar,e1),
init has_VW_es(tomsCar,e2),
init has_es_alt(e1,a3),
init has_es_alt(e2,a4),
init /\VW1: (has_VW_alt(VW1,Alt) ->> defective(Alt));
goal ::
last (has_non_def_alt(dicksCar) && has_non_def_alt(tomsCar)).
% CCALC with SATO finds the following plan for this problem
% | ?- loadf('car-domain-C').
% loading file /v/hank/v32/esra/causation/ccalc/car-domain-C
% loading file /v/hank/v32/esra/causation/ccalc/C
% loading file /v/hank/v32/esra/causation/ccalc/car-pb-C
% 102 atoms, 4444 rules, 1840 clauses (56 new atoms)
% Grounding time: 9200 ms
% Completion time: 510 ms
% Total time: 9710 ms
% yes
% | ?- plan 0.
% calling sato...
%
% 0. defective(a3) defective(a4) has_VW_alt(dicksCar,a3)
% has_VW_alt(tomsCar,a4) has_VW_es(dicksCar,e1) has_VW_es(tomsCar,e2)
% has_es_alt(e1,a3) has_es_alt(e2,a4)
%
% ACTIONS: replaceAlternator(e1,a1)
%
% 1. defective(a3) defective(a4) has_non_def_alt(dicksCar)
% has_VW_alt(dicksCar,a1) has_VW_alt(tomsCar,a4) has_VW_es(dicksCar,e1)
% has_VW_es(tomsCar,e2) has_es_alt(e1,a1) has_es_alt(e2,a4)
%
% ACTIONS: replaceAlternator(e2,a2)
%
% 2. defective(a3) defective(a4) has_non_def_alt(dicksCar)
% has_non_def_alt(tomsCar) has_VW_alt(dicksCar,a1)
% has_VW_alt(tomsCar,a2) has_VW_es(dicksCar,e1) has_VW_es(tomsCar,e2)
% has_es_alt(e1,a1) has_es_alt(e2,a2)
%
% run time (seconds) 0.03
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
=============
Date: Wed, 17 Feb 99
From: Monica Nogueira
To: Ale Provetti
Thank you for taking the time to prepare a representation of the car problem
and sharing it with us.
Here are some questions:
1. Predicate is_a seems to be used with two different semantics
a. is_a(vw,car) seems to mean class vw is a (proper) subclass of class car
b. is_a(i1,vw-rabbit) seems to mean (instance) i1 is an object of class vw-rabbit.
Questions: Do you believe those two meanings should be represented in the same way
(through is_a)?
Is it the standard representation in semantic networks?
We prefer to use two relations, subclass and is_a.
2. We don't understand how the program is going to entail that Tom's car is defective.
Partially because we don't understand what default inheritance here means, and
we also don't fully understand the use of ":". Is it a binary function?
3. We didn't see where instance(P:I) is used, so we don't understand why you need
to declare that.
4. We also would like to know how would you write a relation to diagnose, for example,
what's is wrong with Tom's car. The desirable answer for us would be: Its alternator
is defective.
Looking forward to your clarifications.
=============
Date: Wed, 17 Feb 99
From: Monica Nogueira
To: Esra Erdem
Thank you for sending a representation for the car problem. We looked it over,
but need your help to understand the following points:
1. We are having trouble in understanding what do the relations mean.
Descriptions of the form:
p(X,Y) iff "some property holds for X and Y"
would help us.
2. We want to be able to answer queries about the static state of affairs, e.g.
What's wrong with Tom's car?
Desirable answer: Its alternator is defective!
Is Tom's car defective? Yes
If new information like:
Jim has a Toyota.
is added to the program, we want to be able to infer that the alternator of
Jim's car is not defective.
etc.
We don't know how to obtain this information from your representation, and
would appreciate your help in clarifying that.
=========
Date: Thu, 15 Jul 1999
From: Esra Erdem
To: TAG
I decided to go back to study the car problem introduced by Michael
Gelfond and Monica Nogueira, and came up with a formalization for this
domain. It is attached below with some sample demonstrations.
My main goal was to get an answer to the question "What's wrong with Tom's
car?". This question is presented to CCALC to find a satisfying
interpretation in the presence of the directive
:- show isWrong(X,tomsCar).
This form of the show directive is a new feature introduced in connection
with this example. With this show directive, all instances of
isWrong(X,tomsCar) are filtered from the interpretation computed by a SAT
solver, and displayed to the user. The new version of CCALC has not been
placed on the web yet.
-------------------------------------------------------------------------
% 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)
% (1) is described by the following sort declaration.
:- sorts object >> ((car >> ((vw >> vwRabbit);
toyota));
electricSystem;
alternator;
airCondSystem).
:- variables
X, Y, Z :: object;
C1 :: car;
VW :: vw;
AC :: airCondSystem;
ES :: electricSystem;
Alt :: alternator.
% (2)-(5) are described by the following constant declarations.
:- constants
mikesCar :: toyota;
dicksCar :: vwRabbit;
tomsCar :: vwRabbit;
es(vw) :: electricSystem; % es: vw -> electricSystem
alt(vw) :: alternator; % alt: vw -> alternator
ac(car) :: airCondSystem; % ac: car -> airCondSystem
part(object,object) :: atomicFormula;
partsOK(object) :: atomicFormula;
isWrong(object,object) :: atomicFormula;
defective(object) :: atomicFormula.
% part(X,Y) iff X is a 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.
:- show none.
% transitivity and irreflexivity
part(X,Y) && part(Y,Z) => part(X,Z).
part(X,X) => false.
% X is not a part of Y by default
-part(X,Y) => -part(X,Y).
% If X is a minimal part of Y that is defective, then X is what is wrong
% with Y.
part(X,Y) && defective(X) && partsOK(X) => isWrong(X,Y).
% Nothing is wrong with Y by default.
-isWrong(X,Y) => -isWrong(X,Y).
% If some part X of Z is defective then all parts of Z are not OK.
part(X,Z) && defective(X) => -partsOK(Z).
% None of the parts of X are defective by default.
partsOK(X) => partsOK(X).
% If some part Z of X is defective then X is defective as well.
part(Z,X) && defective(Z) => defective(X).
% X is not defective by default.
-defective(X) => -defective(X).
% Every VW has an ES
true => part(es(VW),VW).
% Every car has an AC
true => part(ac(C1),C1).
% The alternator of a VW is a part of the ES of that VW (describes (5)
true => part(alt(VW),es(VW)).
% Every VW has a defective alternator (describes (6))
true => defective(alt(VW)).
--------------------------------------------------------------------------
% Sample Demonstrations
| ?- loadf('car.h').
% 220 atoms, 1539 rules, 3750 clauses (1110 new atoms)
Grounding time: 350 msec
Completion time: 670 msec
Total time: 1020 msec
yes
% What are defective?
| ?- show defective(X).
true ?
yes
| ?- sat.
calling sato...
run time (seconds) 0.05
Satisfying Interpretation: defective(dicksCar) defective(tomsCar)
defective(alt(dicksCar)) defective(alt(tomsCar)) defective(es(dicksCar))
defective(es(tomsCar))
yes
% What is wrong with Tom's car?
| ?- show isWrong(X,tomsCar).
true ?
yes
| ?- sat.
calling sato...
run time (seconds) 0.05
Satisfying Interpretation: isWrong(alt(tomsCar),tomsCar)
yes
==============
Date: Tue, 20 Jul 1999
From: Esra Erdem
To: TAG
Attached below is a reformalization of the car problem introduced by
Michael Gelfond and Monica Nogueira. This formalization is almost the same
as the one that I sent earlier, except that part/2 is defined in a
different way and the domain description is in the standard logic
programming notation. The use of this notation as an input for ccalc is
possible because of a new include file written by Norm McCain. This file
will be later placed on the ccalc home page.
------------------------------------------------------------------------------
% 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)
:- include 'lp'.
% (1) is described by the following sort declaration.
:- sorts object >> ((car >> ((vw >> vwRabbit);
toyota));
electricSystem;
alternator;
airCondSystem).
:- variables
X, Y, Z :: object;
C1 :: car;
VW :: vw;
AC :: airCondSystem;
ES :: electricSystem;
Alt :: alternator.
% (2)-(5) are described by the following constant declarations.
:- constants
mikesCar :: toyota;
dicksCar :: vwRabbit;
tomsCar :: vwRabbit;
es(vw) :: electricSystem; % es: vw -> electricSystem
alt(vw) :: alternator; % alt: vw -> 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.
% 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.
% part/2 describes the transitive closure of part0/2
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
part0(es(VW),VW) <- true.
% Every car has an AC
part0(ac(C1),C1) <- true.
% The alternator of a VW is a part of the ES of that VW
part0(alt(VW),es(VW)) <- true.
% 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(VW)) <- true.
========
Date: Thu, 29 Jul 1999
From: Michael Gelfond and Monica Nogueira
To: Esra Erdem
We enjoyed reading your CCALC solution of the car problem.
Thanks very much for doing this. We are really learning.
Michael had a Prolog solution of this problem he used in his AI class a
few years ago [available at the "topics" page]. It is very close to yours.
In particular, both make a distinction between "class of alternators"
and a particular alternator and use function symbols to denote
the latter. (This was a main difficulty for students trying to solve
the problem).
We also found the problem interesting in several other ways.
For instance, it gives a nice example of a fairly simple "static" domain
which requires transitive closures for its representation.
It demonstrates a nice interface between taxonomic hierarchy
and what people in the literature call "partonomic hierarchy".
We still do not fully reflect this hierarchy though.
For instance, if car is defective then some of its parts are defective.
But this does not seem to be always true. A part can be defective
but its subparts can be o.k. (The problem can be in the way
it is assembled, etc.)
(There are actually many papers on this subject which we have not
really read. It may make sense to look at them).
Now we really want to better understand your solution,
especially CCALC representation of a hierarchy.
We are not sure, for instance, how you could represent the following in Ccalc:
1. Ask "What kind of car does Mary have?"
2. Can you prove that Mary's car is not a Toyota.
3. Can you remove CWA from some of your sorts and relations?
(We have some comments on how we do it in SMODELS after the Prolog solution).
========
Date: Sun, 1 Aug 1999
From: Esra Erdem and Vladimir Lifschitz
To: Michael Gelfond and Monica Nogueira
Thanks for your comments.
> We are not sure, for instance, how you could represent the following in Ccalc:
>
> 1. Ask "What kind of car does Mary have?"
>
> 2. Can you prove that Mary's car is not a Toyota.
>
> 3. Can you remove CWA from some of your sorts and relations?
> (We have some comments on how we do it in SMODELS after the Prolog solution)
We can introduce a new predicate kind/2 and define it by
kind(VWR,avwRabbit) <- true.
kind(T,atoyota) <- true.
If we remove CWA then we add
-kind(C1,CL) <- not kind(C1,CL).
Here VWR is a variable for vwRabbits, T a variable for toyotas, and
avwRabbit and atoyota are constants of a new sort, "class". CL is a
variable for classes. Then,
- if we declare Mary's car to be a toyota, we can ask what kind of car she
has:
| ?- show kind(marysCar,CL).
true ?
yes
| ?- sat.
calling sato...
run time (seconds) 0.07
Satisfying Interpretation: kind(marysCar,atoyota)
yes
- 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
Here is the domain description:
% 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)
:- include '/u/esra/causation/ccalc/ccalc/lp'.
% (1) is described by the following sort declaration.
:- sorts (object >> ((car >> ((vw >> vwRabbit);
toyota));
electricSystem;
alternator;
airCondSystem));
class.
:- variables
X, Y, Z :: object;
C1 :: car;
CL :: class;
VW :: vw;
VWR :: vwRabbit;
T :: toyota;
AC :: airCondSystem;
ES :: electricSystem;
Alt :: alternator.
% (2)-(5) are described by the following constant declarations.
:- constants
marysCar :: car;
mikesCar :: toyota;
dicksCar :: vwRabbit;
tomsCar :: vwRabbit;
atoyota, avwRabbit :: class;
es(vw) :: electricSystem; % es: vw -> electricSystem
alt(vw) :: alternator; % alt: vw -> 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
part0(es(VW),VW) <- true.
% Every car has an AC
part0(ac(C1),C1) <- true.
% The alternator of a VW is a part of the ES of that VW
part0(alt(VW),es(VW)) <- true.
% 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(VW)) <- true.
% Every VWR is a vwRabbit.
kind(VWR,avwRabbit) <- true.
% Every T is a toyota.
kind(T,atoyota) <- true.
% A car is not of any kind by default.
-kind(C1,CL) <- not kind(C1,CL).
===============
Date: Tue, 17 Aug 1999
From: Monica Nogueira
To: Esra Erdem and Vladimir Lifschitz
Thank you for answering our questions and providing a new solution.
I tried to understand your solution but I am still not sure about:
1. What is the meaning of the "kind" predicate?
2. Why do you need to introduce new sort "class" and predicate "kind"?
You can guess that I am having trouble understanding, as far as C goes,
how to use "sorts". I read the Ccalc manual (from June 10,1999), but
would appreciate if you could give me any other pointers that would
help clarify this construct use.
===============
Date: Sun, 22 Aug 1999
From: Vladimir Lifschitz
To: Monica Nogueira
The questions that you are raising seem to be not so much about ccalc as
about many-sorted languages in logic in general. Here are some remarks on
this general subject.
Imagine that we want to define a first-order language in which we can talk
about mathematical objects of many different kinds: integers, real numbers,
vectors, triangles, etc. There are two choices:
(i) Represent each kind by a unary predicate: integer(x), real(x), etc.
Mathematical facts would be expressed by formulas in which every quantifier
is restricted by one of these predicates. For instance, we would express
that the area of a triangle is a positive real number by
forall x [triangle(x) -> exists y [real(y) & y>0 & area(x,y)]]. (1)
Relationships between these unary predicates would be described by
axioms like
forall x [integer(x) -> real(x)]. (2)
There is another choice:
(ii) Represent each kind by a sort in the syntax of the language. Then,
in addition to variables for general objects (x,y,...) as in approach
(i), we'll have variables for integers (m,n,...), for real numbers
(a,b,...), for triangles (u,v,...), etc. Instead of (1), we would write
forall u exists a [a>0 & area(u,a)].
Axioms like (2) would not be needed at all. Instead, we would specify in
the syntax of the language that "integer" is a subsort of "real", so that
every term of sort "integer" is counted as a term of sort "real".
The second method allows us to express knowledge more concisely. (This
is why it is used in conventional programming languages, where sorts are
called types).
Each of the two methods can be enhanced by "reifying" kinds. (Generally,
to reify some objects means to introduce variables for them.) In
approach (i), to reify kinds means to switch to a syntax like this:
forall x [isa(x,triangle) -> exists y [isa(y,real) & y>0 & area(x,y)]].
Using variables for kinds, we can write axioms like
isa(x,y) & subclass(y,z) -> isa(x,z),
and axioms like (2) become expressible by atomic formulas:
subclass(integer,real).
In approach (ii), a similar enhancement can be achieved by introducing
"classes" as a new sort, and introducing "isa" as a binary relation between
general objects and classes. This new predicate can be defined explicitly:
isa(x,alpha) <-> [exists m(m=x) & alpha=integerClass]
or [exists a(a=x) & alpha=realClass]
or [exists u(u=x) & alpha=triangleClass]
or ...
This is more or less what Esra and I proposed to do for the VW domain in our
last message, except that we wrote "kind" instead if "isa", and used logic
programming instead of first-order logic.
===============
Date: Fri, 27 Aug 1999
From: Monica Nogueira
To: Vladimir Lifschitz
Ufa! This is a Portuguese interjection of great relief. :)
Thank you for the explanation about many-sorted languages.
It helped me to start understanding Ccalc sort construct,
and therefore the solution to the car problem that you and
Esra sent us.
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.
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.
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?"
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".)