2:- module(fol2tptp,[fol2tptp/2,
3 fol2tptp/3,
4 fol2tptpNew/2,
5 fol2tptpNew/3,
6 fol2tptpOld/2,
7 fol2tptpOld/3,
8 printArgs/2]). 9
10:- use_module(semlib(errors),[warning/2]). 11
12
16
17fol2tptp(Conjecture,Stream):- fol2tptpNew(Conjecture,Stream).
18fol2tptp(Axioms,Conjecture,Stream):- fol2tptpNew(Axioms,Conjecture,Stream).
19
20
24
25fol2tptpNew(Formula,Stream):-
26 write(Stream,'fof(nutcracker,conjecture,'),
27 \+ \+ ( numbervars(Formula,0,_),printTPTP(Formula,Stream) ),
28 write(Stream,').'),
29 nl(Stream).
30
31
35
36fol2tptpNew([],Formula,Stream):- !,
37 fol2tptpNew(Formula,Stream).
38
39fol2tptpNew([Axiom|L],Formula,Stream):-
40 write(Stream,'fof(nutcracker,axiom,'),
41 \+ \+ ( numbervars(Axiom,0,_),printTPTP(Axiom,Stream) ),
42 write(Stream,').'), nl(Stream),
43 fol2tptpNew(L,Formula,Stream).
44
45
49
50fol2tptpOld(Formula,Stream):-
51 write(Stream,'input_formula(nutcracker,conjecture,'),
52 \+ \+ ( numbervars(Formula,0,_),printTPTP(Formula,Stream) ),
53 write(Stream,').'),
54 nl(Stream).
55
56
60
61fol2tptpOld([],Formula,Stream):- !,
62 fol2tptpOld(Formula,Stream).
63
64fol2tptpOld([Axiom|L],Formula,Stream):-
65 write(Stream,'input_formula(nutcracker,axiom,'),
66 \+ \+ ( numbervars(Axiom,0,_),printTPTP(Axiom,Stream) ),
67 write(Stream,').'), nl(Stream),
68 fol2tptpOld(L,Formula,Stream).
69
70
74
75printTPTP(some(X,Formula),Stream):- !,
76 write(Stream,'(? ['),
77 write_term(Stream,X,[numbervars(true)]),
78 write(Stream,']: '),
79 printTPTP(Formula,Stream),
80 write(Stream,')').
81
82printTPTP(all(X,Formula),Stream):- !,
83 write(Stream,'(! ['),
84 write_term(Stream,X,[numbervars(true)]),
85 write(Stream,']: '),
86 printTPTP(Formula,Stream),
87 write(Stream,')').
88
89printTPTP(and(Phi,Psi),Stream):- !,
90 write(Stream,'('),
91 printTPTP(Phi,Stream),
92 write(Stream,' & '),
93 printTPTP(Psi,Stream),
94 write(Stream,')').
95
96printTPTP(or(Phi,Psi),Stream):- !,
97 write(Stream,'('),
98 printTPTP(Phi,Stream),
99 write(Stream,' | '),
100 printTPTP(Psi,Stream),
101 write(Stream,')').
102
103printTPTP(imp(Phi,Psi),Stream):- !,
104 write(Stream,'('),
105 printTPTP(Phi,Stream),
106 write(Stream,' => '),
107 printTPTP(Psi,Stream),
108 write(Stream,')').
109
110printTPTP(bimp(Phi,Psi),Stream):- !,
111 write(Stream,'('),
112 printTPTP(Phi,Stream),
113 write(Stream,' <=> '),
114 printTPTP(Psi,Stream),
115 write(Stream,')').
116
117printTPTP(not(Phi),Stream):- !,
118 write(Stream,'~ '),
119 printTPTP(Phi,Stream).
120
121printTPTP(eq(X,Y),Stream):- !,
122 write_term(Stream,X=Y,[numbervars(true)]).
123
124printTPTP(Pred,Stream):-
125 nonvar(Pred),
126 Pred =.. [Sym|Args],
127 write(Stream,Sym),
128 write(Stream,'('),
129 printArgs(Args,Stream),
130 write(Stream,')').
131
132
136
137printArgs([X],Stream):- !,
138 printArg(Stream,X).
139
140printArgs([X|L],Stream):-
141 printArg(Stream,X),
142 write(Stream,','),
143 printArgs(L,Stream).
144
145
149
150printArg(Stream,X):-
151 functor(X,'$VAR',1), !,
152 write_term(Stream,X,[numbervars(true)]).
153
154printArg(Stream,X):-
155 warning('term expexted, found formula: ~p',X),
156 write_term(Stream,X,[numbervars(true)])