9
10twb_pdl_exe('vpdl/vpdl.twb').
11
12entails(Axs,Conc) :-
13 maplist(copy_term,Axs,Axs2),
14 copy_term(Conc,Conc2),
15 twb_pdl_prove(Axs2,Conc2,yes).
16
17twb_pdl_prove(Axioms,Conc,Result) :-
18 19 tmp_file(twb_in,InFile),
20 tmp_file(twb_out,OutFile),
21 tell(InFile),
22 23 free_vars(Conc,ConcVars),
24 ( ConcVars = [] ->
25 Conc2 = Conc
26 ;
27 guess_var_types(ConcVars,Conc,TypedVars),
28 Conc2 = !(TypedVars : Conc)
29 ),
30 31 write('('),
32 twb_write_axioms(Axioms), !,
33 write(') -> ('),
34 twb_write(Conc2), write(').'), nl,
35 told, !,
36 37 twb_pdl_exe(CmdFile),
38 sformat(PCmd,'~w < ~w > ~w 2>&1',[CmdFile,InFile,OutFile]),
39 shell(PCmd,_),
40 41 sformat(TCmd,'grep "Result:Closed" ~w > /dev/null',[OutFile]),
42 ( shell(TCmd,0) ->
43 Result = yes
44 ;
45 46 sformat(ErrCmd,'grep "Fatal" ~w > /dev/null',[OutFile]),
47 ( shell(ErrCmd,0) ->
48 throw(badly_formed_twb_file(InFile))
49 ;
50 51 Result = no
52 )
53 ).
54
55
59
60twb_write(P) :-
61 twb_write_fml(P), !.
62
63twb_write_fml(true) :-
64 write(' (Verum) '), !.
65twb_write_fml(false) :-
66 write(' (Falsum) '), !.
67twb_write_fml(A=B) :-
68 write('( '),
69 twb_write_term(A),
70 write(' == '),
71 twb_write_term(B),
72 write(' )'), !.
73twb_write_fml(A\=B) :-
74 write('~ ( '),
75 twb_write_term(A),
76 write(' == '),
77 twb_write_term(B),
78 write(' )'), !.
79twb_write_fml(P) :-
80 is_atom(P),
81 twb_write_pred(P).
82twb_write_fml(P & Q) :-
83 write('('),
84 twb_write_fml(P),
85 write(' & '),
86 twb_write_fml(Q),
87 write(')').
88twb_write_fml(P | Q) :-
89 write('('),
90 twb_write_fml(P),
91 write(' v '),
92 twb_write_fml(Q),
93 write(')').
94twb_write_fml(P => Q) :-
95 write('('),
96 twb_write_fml(P),
97 write(' -> '),
98 twb_write_fml(Q),
99 write(')').
100twb_write_fml(P <=> Q) :-
101 write('('),
102 twb_write_fml(P),
103 write(' <-> '),
104 twb_write_fml(Q),
105 write(')').
106twb_write_fml(~P) :-
107 write('~ ('),
108 twb_write_fml(P),
109 write(')').
110twb_write_fml(!([]:P)) :-
111 twb_write_fml(P).
112twb_write_fml(!([V:T|Vs]:P)) :-
113 write('( '),
114 twb_write_fml_sols(twb_valuate_var(T,!(Vs:P)),V,'&',true),
115 write(' )'), flush.
116twb_write_fml(?([]:P)) :-
117 twb_write_fml(P).
118twb_write_fml(?([V:T|Vs]:P)) :-
119 write('( '),
120 twb_write_fml_sols(twb_valuate_var(T,?(Vs:P)),V,'v',false),
121 write(' )'), flush.
122twb_write_fml(knows(A,P)) :-
123 write('( ['),
124 write(A),
125 write('] ('),
126 twb_write_fml(P),
127 write('))').
128twb_write_fml(pknows0(E,P)) :-
129 epath_vars(E,Vars),
130 epath_enum_vars(E,En1),
131 epath_elim_impossible_branches(En1,[],En),
132 ( En = (?false) ->
133 write(' (Verum) ')
134 ; En = (?true) ->
135 twb_write_fml(P)
136 ;
137 write('( ['),
138 number_vars(Vars),
139 twb_write_path(En),
140 write('] ('),
141 twb_write_fml(P),
142 write('))')
143 ).
144
145
146twb_valuate_var(T,Fml,V,Res) :-
147 call(T,Val), subs(V,Val,Fml,Res1),
148 copy_fml(Res1,Res2),
149 simplify(Res2,Res).
150
151twb_write_fml_sols(Pred,Var,Sep,_) :-
152 call(Pred,Var,Sol),
153 twb_write_fml(Sol),
154 write(' '), write(Sep), write(' '), fail.
155twb_write_fml_sols(_,_,_,Final) :-
156 twb_write_fml(Final).
157
158twb_write_terms([],_).
159twb_write_terms([T],_) :-
160 twb_write_term(T), !.
161twb_write_terms([T,T2|Ts],Sep) :-
162 twb_write_term(T),
163 write(Sep),
164 twb_write_terms([T2|Ts],Sep).
165
166twb_write_term(T) :-
167 T =.. [F|Args],
168 ( length(Args,0) ->
169 write(F)
170 ;
171 write(F), write('_'),
172 twb_write_terms(Args,'_')
173 ).
174
175twb_write_pred(P) :-
176 P =.. [F|Terms],
177 write(F),
178 (Terms \= [] -> write('__'), twb_write_terms(Terms,'__') ; true).
179
180twb_write_axioms([]) :-
181 write('Verum').
182twb_write_axioms([A]) :-
183 twb_write_fml(A).
184twb_write_axioms([A|Axs]) :-
185 twb_write_fml(A), write(' & '),
186 twb_write_axioms(Axs).
187
188
189twb_write_path(E1 ; E2) :-
190 write('('),
191 twb_write_path(E1),
192 write(' ; '),
193 twb_write_path(E2),
194 write(')').
195twb_write_path(E1 | E2) :-
196 write('('),
197 twb_write_path(E1),
198 write(' U '),
199 twb_write_path(E2),
200 write(')').
201twb_write_path(?(P)) :-
202 write('( ? '),
203 twb_write_fml(P),
204 write(' )').
205twb_write_path(E*) :-
206 write('( * '),
207 twb_write_path(E),
208 write(' )').
209twb_write_path(-VA) :-
210 ( VA = [] ->
211 twb_write_path(?true)
212 ;
213 write('( '),
214 twb_write_vassign(VA),
215 write(' )')
216 ).
217twb_write_path(A) :-
218 agent(A),
219 write(A).
220
221twb_write_vassign([]).
222twb_write_vassign([(X:V)|Xs]) :-
223 write('! '), write(X), write(' <= '), twb_write_term(V), write(' '),
224 twb_write_vassign(Xs)