1add_herbrand_preds((Head :- Body),(Head :- Body1)) :-
2 herbrandize_variables(Body,[],BodyVars,false,_),
3 herbrandize_variables(Head,BodyVars,_,true,Matches),
4 conjoin(Matches,Body,Body1).
5
6
7herbrandize_variables(Term,VarsIn,VarsOut,MatchesIn,MatchesOut) :-
8 builtin(Term) ->
9 VarsOut = VarsIn,
10 MatchesOut = MatchesIn;
11 12 nonvar(Term) ->
13 myfunctor(Term,_,N),
14 herbrandize_args(Term,VarsIn,VarsOut,MatchesIn,MatchesOut,1,N);
15 identical_member(Term,VarsIn) ->
16 VarsOut = VarsIn,
17 MatchesOut = MatchesIn;
18 19 VarsOut = [Term|VarsIn],
20 conjoin(MatchesIn,herbrand(Term),MatchesOut).
21
22herbrandize_args(Term,VarsIn,VarsOut,MatchesIn,MatchesOut,I,N) :-
23 I > N ->
24 VarsOut = VarsIn,
25 MatchesOut = MatchesIn;
26 27 arg(I,Term,Arg),
28 herbrandize_variables(Arg,VarsIn,Vars1,MatchesIn,Matches1),
29 I1 is I + 1,
30 herbrandize_args(Term,Vars1,VarsOut,Matches1,MatchesOut,I1,N).
31
32herbrand_universe(U) :-
33 setof(X,herbrand(X),U).
34
35herbrand_preds([],true).
36herbrand_preds([C|Cs],Wff) :-
37 herbrand_preds(Cs,Wffs),
38 conjoin((herbrand(C):-true),Wffs,Wff).
39
40add_answer_preds((query :- Query),(query :- (Query,nl,nl,write(answer:Vars),nl))) :-
41 !,
42 variables(Query,Vars).
43add_answer_preds(R,R).
44
46
47constants(Wff,L) :-
48 Wff = (A :- B) ->
49 constants(A,L1),
50 constants(B,L2),
51 union(L2,L1,L);
52 Wff = (A , B) ->
53 constants(A,L1),
54 constants(B,L2),
55 union(L2,L1,L);
56 Wff = (A ; B) ->
57 constants(A,L1),
58 constants(B,L2),
59 union(L2,L1,L);
60 Wff = (A : B) ->
61 constants(A,L1),
62 constants(B,L2),
63 union(L2,L1,L);
64 myfunctor(Wff,search,_) -> 65 arg(1,Wff,X),
66 constants(X,L);
67 builtin(Wff) ->
68 L = [];
69 70 myfunctor(Wff,_,N),
71 (N > 0 ->
72 constantize_args(Wff,[],L,1,N);
73 74 L = []).
75
76constantize_args(Term,FnsIn,FnsOut,I,N) :-
77 var(Term) ->
78 FnsOut = FnsIn;
79 atom(Term) ->
80 FnsOut = [Term|FnsIn];
81 I > N ->
82 FnsOut = FnsIn;
83 84 arg(I,Term,ArgI),
85 (var(ArgI) ->
86 Fns1 = [];
87 88 myfunctor(ArgI,_,NI),
89 constantize_args(ArgI,FnsIn,Fns1,1,NI)),
90 I1 is I + 1,
91 constantize_args(Term,Fns1,FnsOut,I1,N).
92
94
95variables(Wff,L) :-
96 Wff = (A :- B) ->
97 variables(A,L1),
98 variables(B,L2),
99 union(L2,L1,L);
100 Wff = (A , B) ->
101 variables(A,L1),
102 variables(B,L2),
103 union(L2,L1,L);
104 Wff = (A ; B) ->
105 variables(A,L1),
106 variables(B,L2),
107 union(L2,L1,L);
108 Wff = (A : B) ->
109 variables(A,L1),
110 variables(B,L2),
111 union(L2,L1,L);
112 myfunctor(Wff,search,_) -> 113 arg(1,Wff,X),
114 variables(X,L);
115 builtin(Wff) ->
116 L = [];
117 118 myfunctor(Wff,_,N),
119 (N > 0 ->
120 variablize_args(Wff,[],L,1,N);
121 122 L = []).
123
124variablize_args(Term,FnsIn,FnsOut,I,N) :-
125 atom(Term) ->
126 FnsOut = FnsIn;
127 var(Term) ->
128 FnsOut = [Term|FnsIn];
129 I > N ->
130 FnsOut = FnsIn;
131 132 arg(I,Term,ArgI),
133 (var(ArgI) ->
134 union([ArgI],FnsIn,Fns1);
135 136 myfunctor(ArgI,_,NI),
137 variablize_args(ArgI,FnsIn,Fns1,1,NI)),
138 I1 is I + 1,
139 variablize_args(Term,Fns1,FnsOut,I1,N).
140
141
142variablize_clause(Clause,Vars) :-
143 ClauseTerm =.. [clause|Clause],
144 variables(ClauseTerm,Vars).
145
146instance([],_,Clause).
147instance(Vars,Cons,Clause) :-
148 myselect(V,Vars,V1s),
149 member(V,Cons),
150 instance(V1s,Cons,Clause).
151
152skolem([],Term,Term).
153skolem([Var|Vars],Term,SkTerm) :-
154 skolem(Vars,Term,Term1),
155 SkTerm=(Var^Term1).
156
157instances(Clause,Terms,Instances) :-
158 variablize_clause(Clause,Vars),
159 skolem(Vars,instance(Vars,Terms,Clause),DoIt),
160 setof(Clause,DoIt,Instances).
161
162instantiation([],_,[]) :-
163 !.
164instantiation(Matrix,[],Matrix) :-
165 !.
166instantiation([Clause|Matrix],Terms,MatrixInstances) :-
167 instances(Clause,Terms,Instances),
168 instantiation(Matrix,Terms,IMatrix),
169 combine_clauses(Instances,IMatrix,MatrixInstances)