2:- module(fol2otter,[fol2otter/2,
3 fol2otter/3,
4 fol2mace/2,
5 fol2mace/3]). 6
7:- use_module(nutcracker(fol2tptp),[printArgs/2]). 8
9
13
14fol2otter(Formula,Stream):-
15 headerOtter(Stream),
16 printOtterFormula(Formula,Stream),
17 footerOtter(Stream).
18
19fol2otter(Axioms,Formula,Stream):-
20 headerOtter(Stream),
21 printOtterFormulas(Axioms,Stream),
22 printOtterFormula(Formula,Stream),
23 footerOtter(Stream).
24
25
29
(Stream):-
31 format(Stream,'set(auto).~n~n',[]),
32 format(Stream,'assign(max_seconds,100).~n~n',[]),
33 format(Stream,'clear(print_proofs).~n~n',[]),
34 format(Stream,'set(prolog_style_variables).~n~n',[]),
35 format(Stream,'formula_list(usable).~n~n',[]).
36
(Stream):-
38 format(Stream,'~nend_of_list.~n',[]).
39
40
44
45fol2mace(Formula,Stream):-
46 headerMace(Stream),
47 printOtterFormula(Formula,Stream),
48 footerMace(Stream).
49
50fol2mace(Axioms,Formula,Stream):-
51 headerMace(Stream),
52 printOtterFormulas(Axioms,Stream),
53 printOtterFormula(Formula,Stream),
54 footerMace(Stream).
55
56
60
(Stream):-
62 format(Stream,'set(auto).~n~n',[]),
63 format(Stream,'clear(print_proofs).~n~n',[]),
64 format(Stream,'set(prolog_style_variables).~n~n',[]),
65 format(Stream,'formula_list(usable).~n~n',[]).
66
(Stream):-
68 format(Stream,'~nend_of_list.~n',[]).
69
70
74
75printOtterFormula(F,Stream):-
76 \+ \+ ( numbervars(F,0,_),
77 printOtter(F,5,Stream) ),
78 format(Stream,'.~n',[]).
79
80
84
85printOtterFormulas([],_).
86
87printOtterFormulas([F|L],Stream):-
88 printOtterFormula(F,Stream),
89 printOtterFormulas(L,Stream).
90
91
95
96printOtter(some(X,Formula),Tab,Stream):- !,
97 write(Stream,'(exists '),
98 write_term(Stream,X,[numbervars(true)]),
99 write(Stream,' '),
100 printOtter(Formula,Tab,Stream),
101 write(Stream,')').
102
103printOtter(all(X,Formula),Tab,Stream):- !,
104 write(Stream,'(all '),
105 write_term(Stream,X,[numbervars(true)]),
106 write(Stream,' '),
107 printOtter(Formula,Tab,Stream),
108 write(Stream,')').
109
110printOtter(and(Phi,Psi),Tab,Stream):- !,
111 write(Stream,'('),
112 printOtter(Phi,Tab,Stream),
113 format(Stream,' & ~n',[]),
114 tab(Stream,Tab),
115 NewTab is Tab + 5,
116 printOtter(Psi,NewTab,Stream),
117 write(Stream,')').
118
119printOtter(or(Phi,Psi),Tab,Stream):- !,
120 write(Stream,'('),
121 printOtter(Phi,Tab,Stream),
122 write(Stream,' | '),
123 printOtter(Psi,Tab,Stream),
124 write(Stream,')').
125
126printOtter(imp(Phi,Psi),Tab,Stream):- !,
127 write(Stream,'('),
128 printOtter(Phi,Tab,Stream),
129 write(Stream,' -> '),
130 printOtter(Psi,Tab,Stream),
131 write(Stream,')').
132
133printOtter(bimp(Phi,Psi),Tab,Stream):- !,
134 write(Stream,'('),
135 printOtter(Phi,Tab,Stream),
136 write(Stream,' <-> '),
137 printOtter(Psi,Tab,Stream),
138 write(Stream,')').
139
140printOtter(not(Phi),Tab,Stream):- !,
141 write(Stream,'-('),
142 printOtter(Phi,Tab,Stream),
143 write(Stream,')').
144
145printOtter(eq(X,Y),_,Stream):- !,
146 write(Stream,'('),
147 write_term(Stream,X,[numbervars(true)]),
148 write(Stream,' = '),
149 write_term(Stream,Y,[numbervars(true)]),
150 write(Stream,')').
151
152printOtter(Pred,_,Stream):-
153 nonvar(Pred),
154 Pred =.. [Sym|Args],
155 write(Stream,Sym),
156 write(Stream,'('),
157 printArgs(Args,Stream),
158 write(Stream,')')