d83_sven_a@tekno.chalmers.se (SVEN AXELSSON) (10/26/90)
I'm trying to write a small DCG/Prolog program demonstrating the
need for belief revision when processing natural language discourse.
I want my natural language understanding system to be able to
reason by default, but I also want it to avoid inconsistencies in
the database, caused by the conflict of information derived by
default at one time with information derived later from axioms which
holds by necessity. The latter information should override the
former, but you can't just let the system delete it. Deleting of a fact
must be followed by the deleting of facts dependent on it.
The idea is to map, by parsing and by forward chaining reasoning,
natural sentences into a 'dynamic' database (a difference list) of
terms of the form 'F because Js' where F is a fact and Js the facts F
depends on (its justification(s)). 'Controlled backtracking' can then
be performed, based on the information on dependencies among
the facts of the database.
Two sample runs (knowledge base and grammar below):
?- discourse([]-C,[tweety,is,a,bird,'.'],[]).
C = [ (has_wings(x1) because animal(x1),can_fly(x1)),
(animal(x1) because bird(x1)),
(can_fly(x1) because bird(x1)),
(bird(x1) because in_text),
(tweety(x1) because in_text)]
?- discourse([]-C,[tweety,is,a,bird,'.',he,is,a,penguin,'.'],[]).
C = [ (~can_fly(x1) because penguin(x1)),
(penguin(x1) because in_text),
(animal(x1) because bird(x1)),
(bird(x1) because in_text),
(tweety(x1) because in_text)]
I wanted this program to be short, illustrative and a *reasonably*
correct implementation of belief revision. Efficiency is not my
concern here, and as (I'm told) belief revision involves many subtleties,
not even strict correctness is very important. Appended below is what
I've come up with so far. Is this *far* too simple?
Please point out inadequaties and make suggestions for improvements,
in terms of correctness as well as cosmetic. Pointers to literature
and other peoples belief revision programs are also welcome.
I very much appreciate your help,
Torbjoern Lager
Department of Linguistics
S-411 29 Gothenburg
Sweden
:- op(1200,xfy,=>).
:- op(1200,xfy,<=).
:- op(1200,xfy,because).
:- op(1200,xfy,:).
:- op(300,fy,~).
% Grammar
discourse(Cn-Cn) --> [].
discourse(C0-Cn) -->
s(C0-C1),['.'],
discourse(C1-Cn).
s(C0-Cn) -->
np(X,C0-C1),
vp(X,C1-Cn).
np(X,Cn-[(tweety(X) because in_text)|Cn]) --> [tweety],
{gensym(x,X)}.
np(X,C0-Cn) --> [a,bird],
% update and maintain dependencies
{solve([(bird(X) because in_text)|C0]-Cn)}.
np(X,C0-Cn) --> [a,penguin],
{solve([(penguin(X) because in_text)|C0]-Cn)}.
np(X,Cn-Cn) --> [he],
% resolve anaphora constructivly proving 'male(X)'
{bc_infer(Cn,male(X))}.
vp(X,C0-Cn) -->
[is],
np(X,C0-Cn).
% Knowledge base
default: bird(X) => can_fly(X).
necessarily: penguin(X) => ~ can_fly(X).
necessarily: animal(X), can_fly(X) => has_wings(X).
necessarily: bird(X) => animal(X).
necessarily: penguin(X) => bird(X).
male(X) <= tweety(X).
% Forward chaining reason maintenance prover
solve(C0-Cn) :-
step(C0-C1),
solve(C1-Cn).
solve(Cn-Cn).
step(C0-[(B because A)|Cn]) :-
(Status:A => B),
true_in(A,C0),
not member((B because _),C0),
negate(B,NegB),
(not member((NegB because _),C0) ->
Cn = C0
;
Status == necessarily,
delete((NegB because _),C0,C1),
delete_consequences(NegB,C1-Cn)).
true_in((A,B),C0) :- !,
true_in(A,C0),
true_in(B,C0).
true_in(A,C0) :-
member((A because Js),C0).
negate(~C,C) :- !.
negate(C,~C).
delete_consequences(A,C0-Cn) :-
find_justifications(C0,A,As),
delete_facts(As,C0-Cn).
delete_facts([A|As],C0-Cn) :-
delete((A because _),C0,C1),
delete_consequences(A,C1-C2),
delete_facts(As,C2-Cn).
delete_facts([],Cn-Cn).
find_justifications(C0,A,Bs) :-
(bagof(B,(member((B because Js),C0),goal_member(A,Js)),Bs)
;
Bs = []).
% Backward chaining prover
bc_infer(T,A) :-
member((A because _),T).
bc_infer(T,A) :-
(A <= Bs ),
bc_infer(T,Bs).
bc_infer(T,(B,Bs)) :-
bc_infer(T,B),
bc_infer(T,Bs).
% Utilities
goal_member(X,(Y,Ys)) :-
!,(X=Y;goal_member(X,Ys)).
goal_member(X,X).
delete(X,[X|Xs],Xs).
delete(X,[Y|Ys],[Y|Zs]) :-
delete(X,Ys,Zs).
gensym(SymbolName,Symbol) :-
(retract(symb_used(SymbolName,N)),!,M is N + 1;
M is 1),
assert(symb_used(SymbolName,M)),
name(SymbolName,X),
name(M,Y),
append(X,Y,Z),
name(Symbol,Z), !.