16
18
19read_kb(Name,Wff) :-
20 concatenate(Name,'.kb',KBFile),
21 read_clauses(KBFile,Wff).
22
23read_ckb(Name,Wff) :-
24 concatenate(Name,'.ckb',CKBFile),
25 read_clauses(CKBFile,Wff).
26
27read_que(Name,Wff) :-
28 concatenate(Name,'.que',QFile),
29 read_clauses(QFile,Wff).
30
31read_clauses(File,Wff) :-
32 open(File,read,Stream),
33 read_wff_loop(Stream,Wff),
34 close(Stream).
35
36read_wff_loop(Stream,Wff) :-
37 read(Stream,Wff1),
38 (Wff1 == end_of_file ->
39 Wff = true;
40 41 read_wff_loop(Stream,Wff2),
42 conjoin(Wff1,Wff2,Wff)).
43
44read_matrix(File,Wff) :-
45 open(File,read,Stream),
46 read_matrix_loop(Stream,Wff),
47 close(Stream).
48
49read_matrix_loop(Stream,Matrix) :-
50 read(Stream,Elem),
51 (Elem == end_of_file ->
52 Matrix = [];
53 54 read_matrix_loop(Stream,L),
55 Matrix = [Elem|L]).
56
59
60write_ckb(File,KB) :-
61 concatenate(File,'.ckb',KBFile),
62 open(KBFile,write,KBStream),
63 concatenate(File,'.que',QFile),
64 open(QFile,write,QStream),
65 write_contrapositives(streams(KBStream,QStream),KB),
66 close(KBStream),
67 close(QStream),
68 get_file_info(KBFile,size,KBFileSize),
69 get_file_info(QFile,size,QFileSize),
70 nl,nl,
71 write(KBFile),write(" written "),write(KBFileSize),writeln(" bytes"),
72 write(QFile), write(" written "),write(QFileSize), writeln(" bytes"),
73 !.
74
75write_cmm(File,Matrix) :-
76 concatenate(File,'.cmm',MFile),
77 open(MFile,write,MStream),
78 write_matrix(MStream,Matrix),
79 close(MStream),
80 !.
81
82write_query(File,Query) :-
83 concatenate(File,'.que',QFile),
84 open(QFile,write,QStream),
85 write_query_only(QStream,Query),
86 close(QStream),
87 !.
88
89write_query_only(Stream,(A,B)) :-
90 !,
91 write_query_only(Stream,A),
92 write_query_only(Stream,B).
93write_query_only(Stream,(A:-B)) :-
94 functor(A,query,_) ->
95 write_clauses(Stream,(A:-B));
96 97 true.
98
99
100write_contrapositives(Streams,(A,B)) :-
101 !,
102 write_contrapositives(Streams,A),
103 write_contrapositives(Streams,B).
104write_contrapositives(streams(KBStream,QStream),(A:-B)) :-
105 functor(A,query,_) ->
106 write_clauses(QStream,(A:-B));
107 108 write_clauses(KBStream,(A:-B)).
109
110
111write_clauses(Stream,(A,B)) :-
112 write_clauses(Stream,A),
113 write_clauses(Stream,B),
114 !.
115write_clauses(Stream,A) :-
116 write(Stream,A),
117 write(Stream,.),
118 nl(Stream),
119 !.
120write_clauses(A) :-
121 File = 'temp.pl',
122 open(File,write,Stream),
123 write_clauses(Stream,A),
124 close(Stream).
125
126
127write_matrix(Stream,[]) :-
128 nl(Stream),
129 !.
130write_matrix(Stream,[E|L]) :-
131 write(Stream,E),
132 write(Stream,.),
133 nl(Stream),
134 write_matrix(Stream,L),
135 !.
136write_matrix(L) :-
137 File = 'temp.pl',
138 open(File,write,Stream),
139 write_matrix(Stream,L),
140 close(Stream).
141
142
143compile_ckb(File) :-
144 concatenate(File,'.ckb',KBFile),
145 compile(KBFile).
146
147compile_query(File) :-
148 concatenate(File,'.que',QFile),
149 compile(QFile).
150
151ask(Name,Query) :-
152 (variables(Query,[]) ->
153 classical_clauses(Query,Q0),
154 cnf(Q0,Q1),
155 make_matrix(Q1,Q2),
156 matrix_reduction(Q2,Q);
157 158 Q = []),
159
160 concatenate(Name,'.cmm',MFile),
161 read_matrix(MFile,Matrix),
162
163 dpttp1((query:-Query),Q,Matrix,Query1:Matrix),
164
165 nl,
166 write('XRay writing query ... '),
167 write_query(Name,Query1),
168 write('done.'),
169
170 nl,
171 write('XRay compiling query ... '),
172 compile_query(Name),
173 write('done.'),
174 nl,
175 !.
176
177tell(Name,Wff) :-
178 read_kb(Name,KB),
179 conjoin(Wff,KB,NewKB),
180 dpttp(Name,NewKB).
181
182write_proved(Proof,ProofEnd) :-
183 write('proved'),
184 verbose_flag ->
185 write(' by:'),
186 write_proof(Proof,ProofEnd);
187 188 length(Proof,X),
189 write(' qed ;-) ':X).
190
191write_proof(Proof,ProofEnd) :-
192 Proof == ProofEnd,
193 !.
194write_proof([X|Y],ProofEnd) :-
195 nl,
196 write(' '),
197 write(X),
198 write_proof(Y,ProofEnd)