PROLOG-REQUEST@SU-SCORE.ARPA (Chuck Restivo, The Moderator) (11/12/86)
PROLOG Digest Wednesday, 12 Nov 1986 Volume 4 : Issue 70
Today's Topics:
Implementation - CProlog 1.5 bug,
LP Library - Examples for Prover,
& Declarative Language Bibliography, Part Q
----------------------------------------------------------------------
Date: 9 Nov 86 00:23:18 GMT
From: Wayne Citrin <citrin@score.stanford.edu>
Subject: Interesting Cprolog 1.5 bug
Here's an interesting bug in C-Prolog 1.5 that I
stumbled upon.
Take the following program:
main :- foo(_), replace_foo, fail.
foo(1).
replace_foo :- retract(foo(_)), assert(foo(2)), !.
(The cut is needed to remove the choice point set up by
the retract, but that's another bug.)
Run this program by issuing the query ?- main.
The program terminates and fails. The call to foo/1 in
main does not set up a choice point because there is only
one clause in foo at the time the call is made. This is
the behavior one would expect.
Now, put the interpreter in debug mode and issue the same
query. The program loops and never terminates. The call
to foo in main now has a choice point, and there is always
a new choice due to the asserted clause.
This actually happened to me yesterday. What use is a
debugger that introduces new bugs?
-- Wayne Citrin
------------------------------
Date: Wed, 5 Nov 86 17:27:39 est
From: David Plaisted <unc!plaisted%unc.csnet@CSNET-RELAY>
Subject: Example files for Prover
% Here are examples for the simplified problem reduction
% format prover. Each one should be in a separate file
% when the prover is used.
% Dave Plaisted
% UNC Chapel Hill
% July 21, 1986
% *******************************************************
% Chang and Lee Example 1
p(g(X,Y),X,Y).
p(X,h(X,Y),Y).
false :- p(k(X),X,k(X)).
p(U,Z,W) :- p(X,Y,U), p(Y,Z,V), p(X,V,W).
p(X,V,W) :- p(X,Y,U), p(Y,Z,V), p(U,Z,W).
% Chang and Lee Example 2
p(e,X,X).
p(X,e,X).
p(X,X,e).
p(a,b,c).
false :- p(b,a,c).
p(U,Z,W) :- p(X,Y,U), p(Y,Z,V), p(X,V,W).
p(X,V,W) :- p(X,Y,U), p(Y,Z,V), p(U,Z,W).
% Chang and Lee Example 3
false :- p(a,e,a).
p(e,X,X).
p(i(X),X,e).
p(U,Z,W) :- p(X,Y,U), p(Y,Z,V), p(X,V,W).
p(X,V,W) :- p(X,Y,U), p(Y,Z,V), p(U,Z,W).
% Chang and Lee Example 4
p(e,X,X).
p(i(X),X,e).
false :- p(a,X,e).
p(U,Z,W) :- p(X,Y,U), p(Y,Z,V), p(X,V,W).
p(X,V,W) :- p(X,Y,U), p(Y,Z,V), p(U,Z,W).
% Chang and Lee Example 5
s(a).
p(e,X,X).
p(X,e,X).
p(X,i(X),e).
p(i(X),X,e).
false :- s(e).
s(Z) :- p(X,i(Y),Z),s(X),s(Y).
p(U,Z,W) :- p(X,Y,U), p(Y,Z,V), p(X,V,W).
p(X,V,W) :- p(X,Y,U), p(Y,Z,V), p(U,Z,W).
% Chang and Lee Example 6
s(b).
p(e,X,X).
p(X,e,X).
p(i(X),X,e).
p(X,i(X),e).
false :- s(i(b)).
s(Z) :- p(X,i(Y),Z),s(X),s(Y).
p(U,Z,W) :- p(X,Y,U), p(Y,Z,V), p(X,V,W).
p(X,V,W) :- p(X,Y,U), p(Y,Z,V), p(U,Z,W).
% Chang and Lee Example 7
p(a).
m(a,s(c),s(b)).
m(X,X,s(X)).
false :- d(a,b).
m(Y,X,Z) :- m(X,Y,Z).
d(X,Z) :- m(X,Y,Z).
d(X,Y) :- p(X),not(d(X,Z)),m(Y,Z,U),d(X,U).
% Chang and Lee Example 8
l(1,a).
d(X,X).
false :- d(X,a),p(X).
d(X,Z) :- d(Y,Z),d(X,Y).
p(f(X)) :- l(1,X),l(X,a).
d(f(X),X) :- l(1,X),l(X,a).
d(g(X),X) :- not(p(X)).
l(1,g(X)) :- not(p(X)).
l(g(X),X) :- not(p(X)).
% Chang and Lee Example 9
% For this one the way the last three rules was
% expressed, was important for efficiency
l(X,f(X)).
false :- l(X,X).
false :- l(X,Y),l(Y,X).
l(Y,X) :- d(X,f(Y)).
l(f(a),X) :- l(a,X),p(X).
d(h(X),X) :- not(p(X)).
p(h(X)) :- not(p(X)).
l(h(X),X) :- not(p(X)).
% A verification condition for Hoare's FIND program
lt(j,i).
le(m,p).
le(p,q).
le(q,n).
false :- le(b(p),b(q)).
le(X,Y) :- not(lt(Y,X)).
le(b(X),b(Y)) :- le(m,X),le(Y,j),le(X,Y).
le(b(X),b(Y)) :- le(i,X),le(Y,n),le(X,Y).
le(b(X),b(Y)) :- le(m,X),lt(X,i),lt(j,Y),le(Y,n).
% A conditional planning problem in situation calculus
% representation (I composed this one)
at(f,s0).
cold(S) :- not(warm(T)).
at(b,walk(b,S)) :- at(a,S).
at(b,drive(b,S)) :- at(a,S).
at(a,walk(a,S)) :- at(b,S).
at(a,drive(a,S)) :- at(b,S).
at(c,skate(c,S)) :- cold(S),at(b,S).
at(b,skate(b,S)) :- cold(S),at(c,S).
at(d,climb(d,S)) :- warm(S),at(b,S).
at(b,climb(b,S)) :- warm(S),at(d,S).
at(d,go(d,S)) :- at(c,S).
at(c,go(c,S)) :- at(d,S).
at(e,go(e,S)) :- at(c,S).
at(c,go(c,S)) :- at(e,S).
at(f,go(f,S)) :- at(d,S).
at(d,go(d,S)) :- at(f,S).
false :- at(a,S).
% Commutativity of join (set intersection); el is set
% membership
not(el(X,p(Y))) :- not(sub(X,Y)).
el(X,p(Y)) :- sub(X,Y).
not(el(X,join(Y,Z))) :- not(el(X,Y)).
el(X,join(Y,Z)) :- el(X,Y),el(X,Z).
el(X,join(Y,Z)) :- el(X,Z),el(X,Y).
false :- eq(join(a,b),join(b,a)).
% rewrites and replacements. The prover does a kind of
% outermost rewriting; the notsub rule is designed to
% insure that the sub(X,Y) replacement before it is only
% done in a montone context, that is, no enclosing
% negations
rewrite(eq(X,Y),and(sub(X,Y),sub(Y,X))).
rewrite(sub(X,Y),or(not(el(g(X,Y),X)),el(g(X,Y),Y))).
rewrite(not(sub(X,Y)),notsub(X,Y)).
replace(notsub(X,Y),and(el(Z,X),not(el(Z,Y)))).
rewrite(el(X,p(Y)),sub(X,Y)).
rewrite(el(X,join(Y,Z)),and(el(X,Y),el(X,Z))).
rewrite(not(eq(X,Y)),or(not(sub(X,Y)),not(sub(Y,X)))).
rewrite(not(el(X,p(Y))),not(sub(X,Y))).
rewrite(not(el(X,join(Y,Z))),or(not(el(X,Y)),not(el(X,Z)))).
rewrite(not(or(X,Y)),and(not(X),not(Y))).
rewrite(not(and(X,Y)),or(not(X),not(Y))).
rewrite(not(not(X)),X).
rewrite(or(X,and(Y,Z)),and(or(X,Y),or(X,Z))).
rewrite(or(and(X,Y),Z),and(or(X,Z),or(Y,Z))).
or(X,Y) :-- prolog(tautology(or(X,Y))).
or(X,Y) :-- X.
or(X,Y) :-- Y.
and(X,Y) :-- X,Y.
% solved July 16 1986 8.4 cpu seconds 8 inferences size 5
% Prolog source code for the tautology checker used in the
% commutativity of set intersection example; needs to be
% directly loaded into C Prolog
tautology(X) :- or_memb(not(Y),X),
or_member(Y,X).
% don't instantiate variables very much
or_memb(not(X),Y) :- var(Y), !, Y=not(X).
or_memb(X,X).
or_memb(Z, or(X,Y)) :-
(or_memb(Z,X) ; or_memb(Z,Y)).
or_member(X,Y) :- var(Y), !, unify(X,Y).
or_member(X,Y) :- unify(X,Y).
or_member(Z, or(X,Y)) :-
(or_member(Z,X) ; or_member(Z,Y)).
% the power set problem; p(X) is the power set of X
not(el(X,p(Y))) :- not(sub(X,Y)).
el(X,p(Y)) :- sub(X,Y).
not(el(X,join(Y,Z))) :- not(el(X,Y)).
el(X,join(Y,Z)) :- el(X,Y),el(X,Z).
el(X,join(Y,Z)) :- el(X,Z),el(X,Y).
replace(false,eq(p(join(a,b)),join(p(a),p(b)))).
rewrite(eq(X,Y),and(sub(X,Y),sub(Y,X))).
rewrite(sub(X,Y),or(not(el(g(X,Y),X)),el(g(X,Y),Y))).
rewrite(not(sub(X,Y)),notsub(X,Y)).
replace(notsub(X,Y),and(el(Z,X),not(el(Z,Y)))).
rewrite(el(X,p(Y)),sub(X,Y)).
rewrite(el(X,join(Y,Z)),and(el(X,Y),el(X,Z))).
rewrite(not(eq(X,Y)),or(not(sub(X,Y)),not(sub(Y,X)))).
rewrite(not(el(X,p(Y))),not(sub(X,Y))).
rewrite(not(el(X,join(Y,Z))),or(not(el(X,Y)),not(el(X,Z)))).
rewrite(not(or(X,Y)),and(not(X),not(Y))).
rewrite(not(and(X,Y)),or(not(X),not(Y))).
rewrite(not(not(X)),X).
rewrite(or(X,and(Y,Z)),and(or(X,Y),or(X,Z))).
rewrite(or(and(X,Y),Z),and(or(X,Z),or(Y,Z))).
or(X,Y) :-- prolog(tautology(or(X,Y))).
or(X,Y) :-- X.
or(X,Y) :-- Y.
and(X,Y) :-- X,Y.
% solved July 16 1986 204 cpu seconds 53 inferences size 14
% solved July 20 1986 with and-or restrictions on splitting,
% false replacement
% no split bound for small proofs, 146.9 seconds, 47
% inferences, size 5, did not seem to use tautology test
% a simple example to illustrate splitting
false :- p,q.
p :- not(r).
p :- r.
q :- not(s).
q :- s.
% schubert's steamroller, almost in the form he gave
w(w).
b(b).
s(s).
f(f).
c(c).
g(g).
a(X) :-- w(X).
a(X) :-- b(X).
a(X) :-- s(X).
a(X) :-- c(X).
a(X) :-- f(X).
p(X) :-- g(X).
m(X,Y) :-- c(X),b(Y).
m(X,Y) :-- b(X),f(Y).
m(X,Y) :-- s(X),b(Y).
m(X,Y) :-- f(X),w(Y).
false :- f(X),w(Y),e(Y,X).
false :- w(Y),g(X),e(Y,X).
false :- b(X),s(Y),e(X,Y).
e(X,Y) :-- b(X),c(Y).
p(h(X)) :-- c(X).
p(i(X)) :-- s(X).
e(X,h(X)) :-- c(X).
e(X,i(X)) :-- s(X).
g(j(X,Y)) :-- a(X),a(Y).
false :- a(Y),e(X,Y),a(X),e(Y,j(X,Y)).
e(X,Y) :- split2(X),p(Y).
split2(X) :-- m(Z,X),a(X),a(Z),split(Z),not(e(X,Z)).
split(Z) :-- e(Z,W),p(W).
% proved July 7-8 1986 2160.7 cpu seconds 6976 inferences
% size bound 42
% on vax 785w(w).
% schubert's steamroller, modified to delay instantiation of
% arguments to j
b(b).
s(s).
f(f).
c(c).
g(g).
a(X) :-- w(X).
a(X) :-- b(X).
a(X) :-- s(X).
a(X) :-- c(X).
a(X) :-- f(X).
p(X) :-- g(X).
m(X,Y) :-- c(X),b(Y).
m(X,Y) :-- b(X),f(Y).
m(X,Y) :-- s(X),b(Y).
m(X,Y) :-- f(X),w(Y).
false :- f(X),w(Y),e(Y,X).
false :- w(Y),g(X),e(Y,X).
false :- b(X),s(Y),e(X,Y).
e(X,Y) :-- b(X),c(Y).
p(h(X)) :-- c(X).
p(i(X)) :-- s(X).
e(X,h(X)) :-- c(X).
e(X,i(X)) :-- s(X).
g(j(X,Y)) :-- not(na(X)),not(na(Y)).
false :- not(na(Y)),not(na(X)),e(X,Y),e(Y,j(X,Y)).
e(X,Y) :- split2(X),p(Y).
split2(X) :- m(Z,X),a(X),a(Z),split(Z),not(e(X,Z)).
split(Z) :- e(Z,W),p(W).
false :-- na(X),a(X).
% proved July 8 1986 572.2 cpu seconds 1340 inferences
% size 42 on vax 785
% proved July 10 1986 447 cpu seconds 897 inferences
% size 56 with splitting ground subgoals near root
% proved July 13-14 415 seconds 692 inferences size 42
% with splitting all ground subgoals, better merge filter
% proved July 16 351 seconds 575 inferences size 42 not
% sure why better, maybe unit simplification
eq(X,X).
eq(Y,X) :- eq(X,Y).
eq(Z,U) :- lat(X,Y,Z), lat(X,Y,U).
eq(Y,U) :- lat(X,Y,Z), lat(X,U,Z).
eq(X,U) :- lat(X,Y,Z), lat(U,Y,Z).
eq(Z,U) :- gre(X,Y,Z), gre(X,Y,U).
eq(Y,U) :- gre(X,Y,Z), gre(X,U,Z).
eq(X,U) :- gre(X,Y,Z), gre(U,Y,Z).
lat(X,Y,a) :- not(lat(X,Y,b)).
lat(X,a,Y) :- not(lat(X,b,Y)).
lat(a,X,Y) :- not(lat(b,X,Y)).
gre(X,Y,a) :- not(gre(X,Y,b)).
gre(X,a,Y) :- not(gre(X,b,Y)).
gre(a,X,Y) :- not(gre(b,X,Y)).
eq(X,V) :- lat(X,Y,Z), gre(X,Y,U), lat(V,W,Z),
not(eq(Y,W)), gre(V,W,U).
false :- eq(a,b).
% proved August 7 1987 size 14 8313 cpu seconds 2371
% inferences about 140 solutions found 4 seconds per
% inference!
------------------------------
Date: Tue 11 Nov 86 20:56:45-PST
From: Chuck Restivo <Restivo@Score.Stanford.EDU>
Subject: Lauren Smith Bibliography, Part Q
QUI60a
Quine W.V.O.
Word and Object
MIT Press, Cambridge, 1960
------------------------------
End of PROLOG Digest
********************