#! /bin/sh
# This is a shell archive. Remove anything before this line, then unpack
# it by saving it into a file and typing "sh file". To overwrite existing
# files, type "sh file -c". You can also feed this as standard input via
# unshar, or by typing "sh 'atp.pl' <<'END_OF_FILE'
X%%% Adam Farquhar 9/1/95
X%%%
X%%% An interpreted model elimination theorem prover.
X%%%
X%%% I use iterative deepening with (1) a filter so that goals found on
X%%% previous iterations are not returned, (2) a test so that if no
X%%% paths are pruned due to the depth cutoff, no further deepening
X%%% will occur, and (3) a method to determine a minimum depth bound
X%%% increment that might result in a new answer being found.
X%%%
X%%% Unification does NOT include an occurs check. This is because I
X%%% want to work with a logic that allows for infinite terms.
X%%%
X
X%%% USAGE
X/***
Xclear
X - clear out database and reset any flags.
Xshow
X - show the internal clauses.
Xprove(Goal)
Xprove(Goal,InitialBound)
Xprove(Goal,InitialBound,Max)
X - try to prove the full FOL Goal, which may be of the form
X Term^Goal, which will cause the variables in Term to be bound.
X prove constructs a clause query(Term) :- Goal and then tries to
X prove query(Term).
Xprove_goal(Goal)
Xprove_goal(Goal,InitialBound)
Xprove_goal(Goal,InitialBound,Max)
X - Use iterative deepening to prove Goal within Max starting with a
X bound of InitialBound. Goal needs to be an atomic formula.
Xprove_goal_bounded(Goal,Ancestors,InitialBound,-Remaining)
Xprove_goal_bounded(+Goal,Ancestors,+Bound,-Remaining)
X - Try to prove Goal within Bound.
Xrule(Head,Body,Cost)
X - Clauses are represented with the predicate rule/3. Calls to
X system predicates may be done by asserting rule/3. E.g., if you
X want to allow for append/3 to be accessed, all you need to do is
X to assert:
X rule(append(X,Y,Z),[],1) :- append(X,Y,Z).
X where [] is the empty body and 1 is the cost of execution.
X
XSYNTAX
X all(X,some(Y,loves(X,Y))).
X a <=> b.
X a <= b and c or d.
X b and c or d => a.
X ~(a and b) <=> ~a or ~b.
X
X***/
X
X%%% BUGS
X%%%
X%%% 9/12/95 No known bugs.
X%%%
X
X%%% CHANGES
X%%% 9/12/95
X%%% * Eliminated builtin. The same effect can be achieved by using
X%%% rule/3. Improved id; Added max, tally/3. Simplified and rewrote
X%%% contrapositives. Eliminated unused code. Tried using ord... for
X%%% ancestor list, but removed it because it slowed things down on the
X%%% current examples. On hpp-ss10d-3, e5(100) takes 1 sec,
X%%% chang_lee_example2 takes 8 sec.
X%%%
X
X%%% TODO
X%%%
X%%% - Figure out how to write apply, holds, inverse, function.
X%%%
X%%% - The clausal form converter seems to reverse the order of
X%%% predicates occasionaly. This can be trouble with builtins like
X%%% is/2, which require certain vars to be bound.
X%%%
X%%% - prove needs a better interface for collecting bindings.
X%%% E.g. if we query some(X,p(X)), then the X gets renamed when
X%%% converting to clausal form, so we don't see the bindings.
X%%%
X%%% - Contrapositives should be careful with builtins. We should
X%%% probably not include them. We also need to be careful with
X%%% ordering in clause formation (see bugs).
X%%%
X%%% - See what the effect of indexing the ancestor list would be. We
X%%% used to have two lists (as did Stickel) -- one for postive and one
X%%% for negative ancestors. The main reason for this was that Stickel
X%%% used the functor not_xxx rather than ~(xxx) to represent negation.
X%%% This made run-time computation of the negation more expensive.
X%%% + I tried using ord_add_element and ord_identical_member for the
X%%% ancestor list. This slowed things down on the example problems,
X%%% none of which have very deep ancestor lists (11 for chang/lee2).
X%%% Perhaps a good binary tree would be worth the effort.
X%%%
X%%% - Should the rules be passed as an argument rather than indexed in
X%%% the database? If so, be careful about variable bindings! This
X%%% would probably be faster for simple examples. For larger
X%%% problems, it would depend on the quality of the indexing
X%%% mechanism. Since we currently lose the principle functor index
X%%% (they are all 'rule') it might still be a win.
X%%%
X%%% - Collect Proof
X%%%
X
X%%% ISSUES
X%%%
X%%% - Should I use member or identical_member when checking for an
X%%% ancestor? Should the test backtrack to look at more ancestors? (I
X%%% don't think so). Should I use subsumes_chk?
X%%%
X
X%% Moved this to my .sicstusrc file.
X%% assertz_new(C) :- C -> true ; assertz(C).
X%% :- assertz_new(library_directory('/a/axf/theorem-provers/me')).
X
X%% :- ensure_loaded(library(clause)).
X:- use_module(clause).
X:- use_module(library(basics)).
X:- use_module(library(lists)).
X:- dynamic rule/3.
X
X%%% Model Elimination Theorem Prover
X%%%
X
Xclear :- abolish(rule/3),
X assert_list(
X [(rule(apply(X,Y),[],1) :- apply(X,Y)),
X (rule(X is Y,[],1) :- X is Y)
X ]).
X
Xshow :- listing(rule/3).
X
Xaxioms([]).
Xaxioms([H|T]) :-
X axiom(H),
X axioms(T).
X
Xaxiom(Fol) :-
X fol_rules(Fol,Clauses),
X assert_list(Clauses).
X
X%%% prove takes an arbitrary FOL statement and tries to prove it.
X%%% The Sentence may be a FOL sentence in which case only success/failure
X%%% is returned, or it can be a term Vars^Sentence, which will cause
X%%% Vars to have the bindings from the successful proofs.
X
Xprove(Sentence) :- prove(Sentence,5).
Xprove(Sentence,InitialBound) :- prove(Sentence,InitialBound,100).
X
Xprove(Sentence0,InitialBound,Max) :-
X (Sentence0 = Vars^Sentence
X ->
X Query = query(Vars)
X ;
X Query = query, Sentence = Sentence0),
X retract_query,
X axiom(Sentence => Query),
X prove_goal(Query,InitialBound,Max).
X
Xretract_query :-
X member(Q,[query,~query,query(_),~query(_)]),
X retractall(rule(Q,_,_)),
X clause(rule(A,B,C),true),
X member(Q,B),
X retract(rule(A,B,C)),
X fail.
Xretract_query.
X
X
Xprove_goal(Goal) :- prove_goal(Goal,5,100).
Xprove_goal(Goal,InitialBound) :- prove_goal(Goal,InitialBound,100).
X
Xprove_goal(Goal,InitialBound,Max) :-
X id(prove_goal_bounded(Goal,[]),InitialBound,Max).
X
Xprove_goal_bounded(Goal,Anc,_B,_B) :-
X %% (optional) If there is an identical ancestor, then we are
X %% in a branch that is doomed to fail, so we can prune it.
X identical_member(Goal, Anc),
X !,
X fail.
Xprove_goal_bounded(Goal,Anc,B0,B) :-
X %% The model elimination reduction operation. The goal is
X %% solved if we find a negated ancestor.
X negate(Goal,Negated),
X identical_member(Negated, Anc),
X tally(1,B0,B).
Xprove_goal_bounded(Goal,Anc,B0,B) :-
X rule(Goal,Body,MinProofCost),
X tally(MinProofCost,B0,B1),
X prove_body(Body,[Goal|Anc],B1,B).
X
Xprove_body([],_,B,B).
Xprove_body([Goal|Goals],Anc,B0,B) :-
X prove_goal_bounded(Goal,Anc,B0,B1),
X prove_body(Goals,Anc,B1,B).
X
X%%% Convert to Clausal Form and add Contrapositives
X%%%
X%%% clausal_form(Fol,Clauses) translates between FOL and Clausal form.
X%%% Each Clause is a term clause(PosAtoms,NegAtoms).
X%%% We use a "rule" form in which everything looks like a horn clause.
X
Xfol_rules(Fol,Rules) :-
X clausal_form(Fol,Clauses),
X clausal_to_rules(Clauses,Rules).
X
Xclausal_to_rules([],[]) :- !.
Xclausal_to_rules([Clause|Clauses],Rules) :-
X contrapositives(Clause,Rules0),
X clausal_to_rules(Clauses,Rules1),
X append(Rules0,Rules1,Rules).
X
Xcontrapositives(clause(Head,Body),C) :-
X negate_list(Head,Not_Head),
X append(Not_Head,Body,Atoms),
X contras(Atoms,Atoms,C).
X
Xcontras([],_,[]).
Xcontras([H|T],Body,[Head_Rule|Tail_Rules]) :-
X negate(H,Not_H),
X delete(Body,H,ThisBody),
X length(Body,Cost),
X Head_Rule = rule(Not_H,ThisBody,Cost),
X contras(T,Body,Tail_Rules).
X
X%%% ITERATIVE DEEPENING
X%%%
X%% The idea for this is From O'Keefe pg66. The iterative deepening
X%% driver (1) only returns a particular solution/tree one time, and
X%% (2) increments the depth bound the minimum amount believed
X%% necessary to find a new solution (using the estimated cost provided
X%% to tally). The tally/3 predicate should be called by the Goal
X%% where appropriate.
X
Xid(Goal,Bound,Max) :- id(Goal,0,Bound,Max).
X
Xid(Goal,PrevBound,Bound,Max) :-
X Bound =< Max,
X flag(depth_cutoff,0),
X apply*(Goal,[Bound,Remaining]),
X Remaining < Bound - PrevBound.
Xid(Goal,_,Bound,Max) :-
X flag(depth_cutoff,Increment),
X Increment > 0,
X Bound1 is Bound + Increment,
X Bound1 =< Max,
X %%format('~Nid: Increasing bound to: ~p.~n',[Bound1]),
X id(Goal,Bound,Bound1,Max).
X
Xtally(N,B0,B) :-
X (B0 >= N % or > ?
X ->
X B is B0 - 1
X ;
X D is N - B0 + 1,
X flag(depth_cutoff,C),
X (C = 0 ; C > D),
X flag(depth_cutoff,D),
X !,
X fail
X ).
X
X%%% General Utilities
X
Xtimed(Goal) :-
X statistics(runtime,[T0,_]),
X call(Goal),
X statistics(runtime,[T1,_]),
X Secs is (T1 - T0) / 1000.0,
X format('~nExecution took ~p seconds.~n',[Secs]).
X
Xapply*(Goal,MoreArgs) :-
X Goal =.. List0,
X append(List0,MoreArgs,List),
X NewGoal =.. List,
X NewGoal.
X
Xapply(Rel,Args) :-
X Goal =.. [Rel|Args],
X Goal.
X
Xassert_list([]).
Xassert_list([H|T]) :- assertz(H),assert_list(T).
X
X%ord_identical_member([H|T],X) :-
X% compare(Order,X,H),
X% ord_identical_member(Order,H,T,X).
X%ord_identical_member(<,_H,_T,_X) :- !, fail.
X%ord_identical_member(=,_,_,_).
X%ord_identical_member(>,_H,T,X) :-
X% ord_identical_member(T,X).
X
Xidentical_member(X,[H|T]) :-
X X == H
X ->
X true
X ;
X identical_member(X,T).
X
X%%% Global flags. There is probably a library/builtin for this.
X
Xflag(Flag,Val) :-
X var(Val)
X ->
X global(Flag,Val)
X ;
X (retractall(global(Flag,_)),
X assert(global(Flag,Val))).
X
X%%% Logic Utilities
X
Xnegate_list([],[]).
Xnegate_list([H|T],[Not_H|Not_T]) :-
X negate(H,Not_H),
X negate_list(T,Not_T).
X
Xnegate(~(G),G) :- !.
Xnegate(G,~(G)).
X
X
X%%% Examples
X
Xe :- e1,e2,e3,e4,e5,e6,e7,e8,e9,
X chang_lee_example1, chang_lee_example2.
X
Xe1 :-
X clear,
X axiom((a or b) and ~(a)),
X prove_goal(b),
X \+ prove_goal(a),
X prove(a or b).
X
Xe2 :- clear,
X axioms(
X [rev([],[]),
X (rev([X|Xs],Zs) <= rev(Xs,Ys) and append(Ys,[X],Zs)),
X append([],Xs,Xs),
X (append([X|Xs],Ys,[X|Zs]) <= append(Xs,Ys,Zs))
X ]),
X prove(rev([a,b,c],[c,b,a])),
X \+ prove(rev([a,b,c],[c,b,a,z])),
X e2(30,497).
X
X%nrev([],[]).
X%nrev([X|Xs],Zs) :- nrev(Xs,Ys),appn(Ys,[X],Zs).
X%appn([],Xs,Xs).
X%appn([X|Xs],Ys,[X|Zs]) :- appn(Xs,Ys,Zs).
X
X%% Naive reverse. The recursion gets quite deep, which means that
X%% checking the ancestor list will be expensive. On such
X%% problems, it would almost certainly pay out to use an indexed
X%% ancestor list. Remember that nrev(30)
X%% takes 496 inferences, add one for query, and we get 497. Starting
X%% with a bound of 497 results in an answer in .27 sec (about 10*
X%% slower than interpreted prolog). Each Iterative deepening step
X%% increases the bound by only 2 or 3. This means that a bound of 496
X%% takes .52 sec (.25+.27) and 494 takes .76sec. It is the last
X%% portion of the tree that is really expensive, so even a bound of
X%% 400 takes 23.7sec. The moral: set the initial bound right the
X%% first time!
X
Xe2(N,B) :-
X length(X,N),
X numbervars(X,0,_),
X timed(prove_goal(rev(X,Y),B,100000)),
X reverse(X,Y).
X
X%% the assert's are done directly because the clausal form reorders goals.
Xe3 :-
X clear,
X assertz(rule(len([],0),[],0)),
X assertz(rule(len([_A|B],N),[len(B,N1),N is N1 + 1],2)),
X prove(X^len([a,b],X)),
X X == 2.
X
Xe4 :-
X clear,
X axioms(
X [q(X) => p(X),
X q(2),
X q(1)]),
X bagof(X,prove(X^p(X)),L),
X (L = [1,2] ; L = [2,1]).
X
Xe5_1(0).
Xe5_1(N) :- N > 0, axiom(p(N)),N1 is N-1, e5_1(N1).
X
X%% This is much faster than I expected. e5(100) takes about 1
X%% second (ss10-3) including converting to clausal form and asserting
X%% the rules.
X
X%% Almost all of the time here is in the bagof or findall. If we just
X%% fail, then it is almost immediate for N=100. For QP,findall is
X
Xe5 :- e5(5).
Xe5(N) :-
X clear, e5_1(N),
X axiom(q(X) <= p(X)),
X axiom(r(X,Y) <= p(X) and q(Y)),
X %%bagof(r(X,Y),prove([X,Y]^r(X,Y)),L),
X bagof(r(X,Y),prove_goal(r(X,Y)),L),
X length(L,Len),
X Len =:= N*N.
X
Xe6 :- clear,
X axioms(
X [p(X) <= apply(format,['APPLY: ~p~n',[X]]) and q(X),
X q(1),
X q(2)]),
X bagof(X,prove(X^p(X)),L),
X format('Should have done APPLY on ~p.~n',[L]).
X
Xe7 :- clear,
X axiom(a or b or c),
X axiom(~c),
X prove(a or b),
X \+ prove(a or c).
X
Xe8 :- clear,
X axiom(a or b or c),
X prove(a or b or c),
X \+ prove(a or b),
X \+ prove(b or c),
X \+ prove(a or c).
X
Xe9 :- clear,
X prove(~(a and b) <=> ~a or ~b).
X
Xe10 :- clear,
X axiom(p(X) or q(X) <= r(X)),
X axiom(r(a) and r(b)),
X prove(X^(p(X) or q(X))),
X \+ prove(p(a)),
X \+ prove(p(b)),
X \+ prove(q(a)),
X \+ prove(q(b)),
X \+ prove(p(a) or q(b)),
X prove(p(a) or q(a)),
X prove(p(b) or q(b)).
X
Xchang_lee_example1 :-
X nl,
X write(chang_lee_example1),
X clear,
X axioms([
X p(g(X,Y),X,Y),
X p(X,h(X,Y),Y),
X (p(U,Z,W) <= p(X,Y,U) and p(Y,Z,V) and p(X,V,W)),
X (p(X,V,W) <= p(X,Y,U) and p(Y,Z,V) and p(U,Z,W)),
X (query(X) <= p(k(X),X,k(X)))
X ]),
X fail. % clear stack used in compilation
Xchang_lee_example1 :-
X %% there are several solutions, at lest one of which results
X %% in a circular term. We used to get the non-circular one
X %% first, but now the order is changed and we get the circular
X %% one.
X prove_goal(query(_)).
X
Xchang_lee_example2 :-
X nl,
X write(chang_lee_example2),nl,
X clear,
X axioms(
X [p(e,X,X),
X p(X,e,X),
X p(X,X,e),
X p(a,b,c),
X (p(U,Z,W) <= p(X,Y,U) and p(Y,Z,V) and p(X,V,W)),
X (p(X,V,W) <= p(X,Y,U) and p(Y,Z,V) and p(U,Z,W)),
X (query <= p(b,a,c))
X ]),
X fail.
Xchang_lee_example2 :-
X prove_goal(query).
X
END_OF_FILE
if test 12934 -ne `wc -c <'atp.pl'`; then
echo shar: \"'atp.pl'\" unpacked with wrong size!
fi
# end of 'atp.pl'
fi
if test -f 'clause.pl' -a "${1}" != "-c" ; then
echo shar: Will not clobber existing file \"'clause.pl'\"
else
echo shar: Extracting \"'clause.pl'\" \(18663 characters\)
sed "s/^X//" >'clause.pl' <<'END_OF_FILE'
X% File : CLAUSE
X% Author : R.A.O'Keefe
X% Updated: 10 March 1984
X% Purpose: Convert a formula in FOPC to clausal form.
X% Needs : ord_union/3 from UTIL:ORDSET.PL.
X
X
X:- module(clause,
X [clausal_form/2,
X clausal_form_of_negation/2,
X units_separated/4,
X all/2,
X some/2,
X (=>)/2,
X (<=)/2,
X (<=>)/2,
X %if/3,
X and/2,
X or/2,
X (~)/1
X ]).
X
X
X:- use_module(library(ordsets)).
X
X/*----------------------------------------------------------------------
X
X This module has three entry points:
X clausal_form(Formula, Clauses)
X clausal_form_of_negation(Formula, Clauses)
X units_separated(Clauses, PosUnits, NegUnits, NonUnits)
X
X The Formula is an , where
X ::= all(, )
X | some(, )
X | =>
X | <=>
X | if(,,)
X | and
X | or
X | ~
X |
X
X ::= (,...,)
X
X ::=
X |
X | (,...,)
X
X The Clauses are a sentence, where
X ::= [] (true)
X | . (and)
X
X ::= clause(, )
X ::= [] | .
X
X Note that this representation of a clause is not quite the
X usual one. clause([a,b,c], [d,e,f]) represents
X a v b v c <- d & e & f
X or, if you don't like "Kowalski form",
X a v b v c v ~d v ~e v ~f
X
X The reason for the two entry points is that the formula may
X contain free variables, these are to be understood as being
X universally quantified, and the negation of the universal
X closure of a formula is not at all the same thing as the
X universal closure of the negation!
X
X units_separated takes a list of clauses such as the other two predicates
X might produce, and separates them into a list of positive unit clauses
X (represented just by s), a list of negative unit clauses (also
X represented by their single s), and a list of non-unit clauses.
X Some theorem provers might find this separation advantageous, but it is
X not buillt into clausal_form becauses some provers would not benefit.
X
X----------------------------------------------------------------------*/
X
X:- public
X clausal_form/2,
X clausal_form_of_negation/2,
X units_seaparated/4.
X
X:- mode
X clausal_form(+, -),
X clausal_form_of_negation(+, -),
X pass_one(+, -),
X pass_one(+, +, -),
X pass_one(+, -, +, +, -),
X term_one(+, +, +, -),
X term_one(+, +, +, +, -),
X pass_two(+, -),
X pass_two_pos(+, -),
X pass_two_pos(+, -, +, +),
X term_two(+, -, +),
X term_var(+, +, -),
X term_two(+, +, +, +),
X pass_two_neg(+, -, +, +),
X sent_and(+, +, -),
X sent_or(+, +, -),
X units_separated(+, -, -, -),
X contains(+, ?),
X literally_contains(+, +),
X does_not_literally_contain(+, ?).
X
X
X:- op(700, xfx, [contains,literally_contains,does_not_literally_contain]).
X:- op(910, fy, ~).
X:- op(920, xfy, and).
X:- op(930, xfy, or).
X:- op(940, xfx, [=>, <=>, <=]).
X
X
Xunits_separated([], [], [], []).
Xunits_separated([clause([],[Neg])|Clauses], PosL, [Neg|NegL], NonL) :- !,
X units_separated(Clauses, PosL, NegL, NonL).
Xunits_separated([clause([Pos],[])|Clauses], [Pos|PosL], NegL, NonL) :- !,
X units_separated(Clauses, PosL, NegL, NonL).
Xunits_separated([Clause|Clauses], PosL, NegL, [Clause|NonL]) :-
X units_separated(Clauses, PosL, NegL, NonL).
X
X
Xclausal_form(Formula, Clauses) :-
X pass_one(Formula, ClosedAndImplicationFree),
X pass_two(ClosedAndImplicationFree, Clauses).
X
X
Xclausal_form_of_negation(Formula, Clauses) :-
X pass_one(Formula, ClosedAndImplicationFree),
X pass_two(~ClosedAndImplicationFree, Clauses).
X
X
X/*----------------------------------------------------------------------
X
X The first pass over the formula does two things.
X 1a. It locates the free variables of the formula.
X 2. It applies the rules
X A => B --> B v ~A
X A <=> B --> (B v ~A) /\ (A v ~B)
X if(A,B,C) --> (B v ~A) /\ (A v C)
X to eliminate implications. Even in a non-clausal
X theorem prover this can be a good idea, eliminating
X <=> and if is essential if each subformula is to
X have a definite parity, and that in turn is vital
X if we are going to replace existential quantifiers
X by Skolem functions.
X 1b. It adds explicit quantifiers for the free variables.
X The predicate which does all this is pass_one/5:
X pass_one(+Formula, % The original formula
X -Translation, % its implication-free equivalent
X +Bound, % The binding environment
X +Free0, % The variables known to be free
X -Free) % Free0 union Formula's free variables
X The binding environment just tells us which variables occur in quantifiers
X dominating this subformula, it doesn't matter yet whether they're
X universal or existential.
X
X The translated formula is still an , although there are practical
X advantages to be gained by adopting a slightly different representation,
X but the neatness of being able to say that
X pass_one(F, G) --> pass_one(G, G)
X outweighs them.
X
X----------------------------------------------------------------------*/
X
Xpass_one(Formula, ClosedAndImplicationFree) :-
X pass_one(Formula, ImplicationFree, [], [], FreeVariables),
X pass_one(FreeVariables, ImplicationFree, ClosedAndImplicationFree).
X
X
Xpass_one([], Formula, Formula).
Xpass_one([Var|Vars], Formula, all(Var,Closure)) :-
X pass_one(Vars, Formula, Closure).
X
X
Xpass_one(all(Var,B), all(Var,D), Bound, Free0, Free) :- !,
X pass_one(B, D, [Var|Bound], Free0, Free).
Xpass_one(some(Var,B), some(Var,D), Bound, Free0, Free) :- !,
X pass_one(B, D, [Var|Bound], Free0, Free).
Xpass_one(A and B, C and D, Bound, Free0, Free) :- !,
X pass_one(A, C, Bound, Free0, Free1),
X pass_one(B, D, Bound, Free1, Free).
Xpass_one(A or B, C or D, Bound, Free0, Free) :- !,
X pass_one(A, C, Bound, Free0, Free1),
X pass_one(B, D, Bound, Free1, Free).
Xpass_one(A => B, D or ~C, Bound, Free0, Free) :- !,
X pass_one(A, C, Bound, Free0, Free1),
X pass_one(B, D, Bound, Free1, Free).
Xpass_one(A <= B, C, Bound, Free0, Free) :- !,
X pass_one(B => A, C, Bound, Free0, Free).
Xpass_one(A <=> B, (D or ~C) and (C or ~D), Bound, Free0, Free) :- !,
X pass_one(A, C, Bound, Free0, Free1),
X pass_one(B, D, Bound, Free1, Free).
Xpass_one(if(T,A,B), (C or ~U) and (D or U), Bound, Free0, Free) :- !,
X pass_one(T, U, Bound, Free0, Free1),
X pass_one(A, C, Bound, Free1, Free2),
X pass_one(B, D, Bound, Free2, Free).
Xpass_one(~A, ~C, Bound, Free0, Free) :- !,
X pass_one(A, C, Bound, Free0, Free).
Xpass_one(Atom, Atom, Bound, Free0, Free) :-
X % An Atom is "anything else". If Atoms were explicitly flagged,
X % say by being written as +Atom, we wouldn't need those wretched
X % cuts all over the place. The same is true of pass_two.
X term_one(Atom, Bound, Free0, Free).
X
X
X% term_one/4 scans a term which occurs in a context where some
X% variables are Bound by quantifiers and some free variables (Free0)
X% have already been discovered. Free is returned as the union of the
X% free variables in this term with Free0. Note that though we call
X% does_not_literally_contain twice, it is doing two different things.
X% The first call determines that the variable is free. The second
X% call is part of adding an element to a set, which could perhaps have
X% been a binary tree or some other data structure.
X
Xterm_one(Term, Bound, Free0, Free) :-
X nonvar(Term),
X functor(Term, _, Arity),
X !,
X term_one(Arity, Term, Bound, Free0, Free).
Xterm_one(Var, Bound, Free0, [Var|Free0]) :-
X Bound does_not_literally_contain Var,
X Free0 does_not_literally_contain Var,
X !.
Xterm_one(_, _, Free0, Free0).
X
Xterm_one(0, _, _, Free0, Free0) :- !.
Xterm_one(N, Term, Bound, Free0, Free) :-
X arg(N, Term, Arg),
X term_one(Arg, Bound, Free0, Free1),
X M is N-1, !,
X term_one(M, Term, Bound, Free1, Free).
X
X
X/*----------------------------------------------------------------------
X
X pass_two does the following in one grand sweep:
X 1. The original formula might have used the same variable in any
X number of quantifiers. In the output, each quantifier gets a
X different variable.
X 2. But existentally quantified variables are replaced by new Skolem
X functions, not by new variables. As a result, we can simply drop
X all the quantifiers, every remaining variable is universally
X quantified.
X 3. The rules
X ~ all(V, F) --> some(V, ~F)
X ~ some(V, F) --> all(V, ~F)
X ~ (A and B) --> ~A or ~B
X ~ (A or B) --> ~A and ~B
X ~ ~ A --> A
X are applied to move negations down in front of atoms.
X 4. The rules
X A or A --> A
X A or ~A --> true
X A or true --> true
X A or false --> A
X (A or B) or C --> A or (B or C)
X (A and B) or C --> (A or C) and (B or C)
X A or (B and C) --> (A or B) and (A or C)
X A and true --> A
X A and false --> false
X (A and B) and C --> A and (B and C)
X are applied to the clauses which we build as we work our
X way back up the tree. The rules
X A and A --> A
X A and ~A --> false
X A and (~A or B) --> A and B
X are NOT applied. This is best done, if at all, after all the
X clauses have been generated. The last two rules are special
X cases of resolution, so it is doubtful whether it is worth
X doing them at all.
X
X The main predicate is pass_two_pos/4:
X pass_two_pos(+Formula, % The formula to translate
X -Translation, % its translation
X +Univ, % universal quantifiers in scope
X +Rename) % how to rename variables
X Rename is var | var(Old,New,Rename), where Old is a source variable,
X and New is either a new variable (for universal quantifiers) or a
X Skolem function applied to the preceding new variables (for existential
X quantifiers). Univ is those New elements of the Rename argument which
X are variables. pass_two_neg produces the translation of its Formula's
X *negation*, this saves building the negation and then handling it.
X
X----------------------------------------------------------------------*/
X
Xpass_two(ClosedAndImplicationFree, ClausalForm) :-
X pass_two_pos(ClosedAndImplicationFree, PreClausalForm, [], var),
X pass_two_pos(PreClausalForm, ClausalForm).
X
X
X% pass_two_pos/2 does two things. First, if there was only one clause,
X% pass_two_pos/4 wouldn't have wrapped it up in a list. This we do here.
X% Second, if one of the clauses is "false", we return that as the only
X% clause. This would be the place to apply A & A --> A.
X
Xpass_two_pos(clause(P,N), [clause(P,N)]) :- !.
Xpass_two_pos(Sentence, [clause([],[])]) :-
X Sentence contains clause([],[]),
X !.
Xpass_two_pos(Sentence, Sentence).
X
X
Xpass_two_pos(all(Var,B), Translation, Univ, Rename) :- !,
X pass_two_pos(B, Translation, [New|Univ], var(Var,New,Rename)).
Xpass_two_pos(some(Var,B), Translation, Univ, Rename) :- !,
X gensym('f-', SkolemFunction),
X SkolemTerm =.. [SkolemFunction|Univ],
X pass_two_pos(B, Translation, Univ, var(Var,SkolemTerm,Rename)).
Xpass_two_pos(A and B, Translation, Univ, Rename) :- !,
X pass_two_pos(A, C, Univ, Rename),
X pass_two_pos(B, D, Univ, Rename),
X sent_and(C, D, Translation).
Xpass_two_pos(A or B, Translation, Univ, Rename) :- !,
X pass_two_pos(A, C, Univ, Rename),
X pass_two_pos(B, D, Univ, Rename),
X sent_or(C, D, Translation).
Xpass_two_pos(~A, Translation, Univ, Rename) :- !,
X pass_two_neg(A, Translation, Univ, Rename).
Xpass_two_pos(true, [], _, _) :- !.
Xpass_two_pos(false, clause([],[]), _, _) :- !.
Xpass_two_pos(Atom, clause([Renamed],[]), _, Rename) :-
X % An Atom is "anything else", hence the cuts above.
X term_two(Atom, Renamed, Rename).
X
X
Xpass_two_neg(all(Var,B), Translation, Univ, Rename) :- !,
X gensym('g-', SkolemFunction),
X SkolemTerm =.. [SkolemFunction|Univ],
X pass_two_neg(B, Translation, Univ, var(Var,SkolemTerm,Rename)).
Xpass_two_neg(some(Var,B), Translation, Univ, Rename) :- !,
X pass_two_neg(B, Translation, [New|Univ], var(Var,New,Rename)).
Xpass_two_neg(A and B, Translation, Univ, Rename) :- !,
X pass_two_neg(A, C, Univ, Rename),
X pass_two_neg(B, D, Univ, Rename),
X sent_or(C, D, Translation).
Xpass_two_neg(A or B, Translation, Univ, Rename) :- !,
X pass_two_neg(A, C, Univ, Rename),
X pass_two_neg(B, D, Univ, Rename),
X sent_and(C, D, Translation).
Xpass_two_neg(~A, Translation, Univ, Rename) :- !,
X pass_two_pos(A, Translation, Univ, Rename).
Xpass_two_neg(true, clause([],[]), _, _) :- !.
Xpass_two_neg(false, [], _, _) :- !.
Xpass_two_neg(Atom, clause([],[Renamed]), _, Rename) :-
X % An Atom is "anything else", hence the cuts above.
X term_two(Atom, Renamed, Rename).
X
X
X
Xterm_two(OldTerm, NewTerm, Rename) :-
X nonvar(OldTerm),
X functor(OldTerm, FunctionSymbol, Arity),
X functor(NewTerm, FunctionSymbol, Arity),
X !,
X term_two(Arity, OldTerm, NewTerm, Rename).
Xterm_two(OldVar, NewTerm, Rename) :-
X term_var(Rename, OldVar, NewTerm).
X
X
Xterm_var(var(Old,New,_), Var, New) :-
X Old == Var,
X !.
Xterm_var(var(_,_,Rest), Var, New) :-
X term_var(Rest, Var, New).
X
X
Xterm_two(0, _, _, _) :- !.
Xterm_two(N, OldTerm, NewTerm, Rename) :-
X arg(N, OldTerm, OldArg),
X term_two(OldArg, NewArg, Rename),
X arg(N, NewTerm, NewArg),
X M is N-1, !,
X term_two(M, OldTerm, NewTerm, Rename).
X
X
X/*----------------------------------------------------------------------
X
X sent_and(S1, S2, "S1 and S2")
X sent_or(S1, S2, "S1 or S2")
X perform the indicated logical operations on clauses or sets of
X clauses (sentences), using a fair bit of propositional reasoning
X (hence our use of "literally" to avoid binding variables) to try
X to keep the results simple. There are several rules concerning
X conjunction which are *not* applied, but even checking for
X A and A --> A
X would require us to recognise alphabetic variants of A rather
X than literal identity. So far the naivety abount conjunction
X has not proved to be a practical problem.
X
X----------------------------------------------------------------------*/
X
Xsent_or(clause(P1,_), clause(_,N2), []) :-
X P1 contains Atom,
X N2 literally_contains Atom,
X !.
Xsent_or(clause(_,N1), clause(P2,_), []) :-
X N1 contains Atom,
X P2 literally_contains Atom,
X !.
Xsent_or(clause(P1,N1), clause(P2,N2), clause(P3,N3)) :- !,
X ord_union(P1, P2, P3),
X ord_union(N1, N2, N3).
Xsent_or([], _, []) :- !.
Xsent_or(_, [], []) :- !.
Xsent_or([Clause|Clauses], Sentence, Answer) :- !,
X sent_or(Sentence, Clause, X),
X sent_or(Clauses, Sentence, Y),
X sent_and(X, Y, Answer).
Xsent_or(Sentence, [Clause|Clauses], Answer) :- !,
X sent_or(Sentence, Clause, X),
X sent_or(Clauses, Sentence, Y),
X sent_and(X, Y, Answer).
X
X
Xsent_and([], Sentence, Sentence) :- !.
Xsent_and(Sentence, [], Sentence) :- !.
Xsent_and([H1|T1], [H2|T2], [H1,H2|T3]) :- !,
X sent_and(T1, T2, T3).
Xsent_and([H1|T1], Clause, [Clause,H1|T1]) :- !.
Xsent_and(Clause, [H2|T2], [Clause,H2|T2]) :- !.
Xsent_and(Clause1, Clause2, [Clause1,Clause2]).
X
X
X[Head|_] contains Head.
X[_|Tail] contains Something :-
X Tail contains Something.
X
X
X[Head|_] literally_contains Something :-
X Head == Something,
X !.
X[_|Tail] literally_contains Something :-
X Tail literally_contains Something.
X
X
X[] does_not_literally_contain Anything.
X[Head|Tail] does_not_literally_contain Something :-
X Head \== Something,
X Tail does_not_literally_contain Something.
X
X
X/*----------------------------------------------------------------------
X Debugging kit.
X portray_sentence(ListOfClauses)
X displays a list of clauses, one per line.
X portray_a_clause(Clause)
X displays a single clause in "Kowalski notation"
X t(Formula)
X translates a formula and prints the result.
X*/
X:- public
X t1/0,t9/0,t/1.
X
X
Xportray_sentence([Clause]) :- !,
X portray_a_clause(Clause),
X nl.
Xportray_sentence([Clause|Clauses]) :-
X portray_a_clause(Clause),
X write(' AND'), nl,
X portray_sentence(Clauses).
Xportray_sentence([]) :-
X write('TRUE'), nl.
X
X
Xportray_a_clause(clause(PosAtoms, NegAtoms)) :-
X numbervars(PosAtoms, 0, N),
X numbervars(NegAtoms, N, _),
X portray_a_clause(PosAtoms, ' v '),
X write(' <- '),
X portray_a_clause(NegAtoms, ' & '),
X fail.
Xportray_a_clause(_).
X
X
Xportray_a_clause([Atom], _) :- !,
X print(Atom).
Xportray_a_clause([Atom|Atoms], Separator) :-
X print(Atom), write(Separator),
X portray_a_clause(Atoms, Separator).
Xportray_a_clause([], _) :-
X write([]).
X
X
Xt(X) :-
X clausal_form(X, Y),
X portray_sentence(Y).
X
Xt1 :- t((a=>b) and (b=>c) and (c=>d) and (d=>a) => (a<=>d)).
X
Xt2 :- t(continuous(F,X) <=> all(Epsilon, Epsilon > 0 =>
X some(Delta, Delta > 0 and all(Y,
X abs(Y-X) < Delta => abs(val(F,Y)-val(F,X)) < Epsilon
X )))).
X
Xt3 :- clausal_form_of_negation(
X ( subset(S1,S2) <=> all(X, member(X,S1) => member(X,S2) )) =>
X ( subset(T1,T2) and subset(T2,T3) => subset(T1,T3) ) ,Y),
X portray_sentence(Y).
X
Xt4 :- t(subset(T1,T2) and subset(T2,T3) => subset(T1,T3)).
X
X
Xt5 :- t((a=>b) and (b=>c)).
X
Xt6 :- t(~(a and b)).
X
Xt7 :- t((a and b) or c).
X
Xt8 :- t((a and b) or (a and ~b) or (~a and b) or (~a and ~b)).
X
Xt9 :- t(
X (true(P) <=> t(w0,P)) and
X (t(W1,P1 and P2) <=> t(W1,P1) and t(W1,P2)) and
X (t(W1,P1 or P2) <=> t(W1,P1) or t(W1,P2)) and
X (t(W1,P1 => P2) <=> (t(W1,P1) => t(W1,P2))) and
X (t(W1,P1 <=> P2) <=> (t(W1,P1) <=> t(W1,P2))) and
X (t(W1,~P1) <=> ~t(W1,P1)) and
X (t(W1,know(A1,P1)) <=> all(W2,k(A1,W1,W2)=>t(W2,P1))) and
X k(A1,W1,W1) and
X (k(A1,W1,W2) => (k(A1,W2,W3) => k(A1,W1,W3))) and
X (k(A1,W1,W2) => (k(A1,W1,W3) => k(A1,W2,W3))) and
X (t(W1,know(A,P)) <=> all(W2,k(A,W1,W2) => t(W2,P)))
X ).
X
X/*----------------------------------------------------------------------*/
X
X
X% File : GENSYM.PL
X% Author : Lawrence Byrd?
X% Updated: 21 February 1984
X% Purpose: create new atoms
X% Needs : append/3.
X
X:- use_module(library(lists)).
X
X:- public
X cgensym/2,
X concat/3,
X gensym/2.
X
X:- mode
X cgensym(+, ?),
X concat(+, +, ?),
X gensym(+, ?).
X
X% gensym(Prefix, V)
X% binds V to a new atom whose name begins with Prefix and ends with a
X% number. E.g. gensym(a,X), gensym(a,Y), gensym(a,Z) might bind
X% X to a1, Y to a2, Z to a3. It only succeeds once per call, to get
X% another binding for V you have to call it again.
X
Xgensym(Prefix, V) :-
X var(V),
X atomic(Prefix),
X ( retract(flag(gensym(Prefix), M))
X | M = 0
X ),
X N is M+1,
X asserta(flag(gensym(Prefix), N)),
X concat(Prefix, N, V),
X !.
X
X
X% cgensym(Prefix, V)
X% binds V to a new atom unless it is already bound. Thus
X% cgensym(a, fred) would succeed, but cgensym(a, X) would bind
X% X to a new atom, maybe a4. "c" standard for "conditional".
X
Xcgensym(Prefix, V) :-
X nonvar(V), !,
X atomic(V),
X atomic(Prefix).
Xcgensym(Prefix, V) :-
X gensym(Prefix, V).
X
X
X% concat(Name1, Name2, Name3)
X% is like append on atoms. That is, it appends the name of Name1 and
X% the name of Name2, and binds Name3 to the atom named by the result.
X% Unlike append, it will only work one way round. Examples:
X% concat(a, b, ab), concat(10, 23, 1023), concat(gs, 46, gs46).
X% concat(04, 05, 405)*??*
X
Xconcat(N1, N2, N3) :-
X name(N1, Ls1),
X name(N2, Ls2),
X append(Ls1, Ls2, Ls3),
X name(N3, Ls3).
X
X
X
X
END_OF_FILE
if test 18663 -ne `wc -c <'clause.pl'`; then
echo shar: \"'clause.pl'\" unpacked with wrong size!
fi
# end of 'clause.pl'
fi
echo shar: End of shell archive.
exit 0