1:- module(fol_test_formula, []). 2
3:- use_module(util('fol-prover')). 4
5:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<-'). 6:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<--'). 7:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<-->'). 8:- current_op(P, T, (->)), member(T,[xfy, yfx, xfx]), op(P, T, '<->'). 9:- op(200, fy, ~). 10:- op(400, yfx, &). 11
12:- discontiguous invalid_formula/2. 13:- discontiguous valid_formula/2. 14:- discontiguous unsatisfiable_formula/2. 15
17
23
28
32test_prove(F, Expected):- nb_setval(formula_count, 0),
33 call(F, K, P),
34 nb_getval(formula_count, N),
35 N0 is N + 1,
36 nb_setval(formula_count, N0),
37 fol_prover:prove(P, R),
38 ( R \== Expected ->
39 nl,
40 writeln(unexpected : R),
41 \+ \+ (numbervars(P), format("~w : ~w\n", [K, P]))
42 ; true
43 ),
44 fail.
45test_prove(_, _):- nb_getval(formula_count, N),
46 format("\n** ~w formulae tested.\n", [N]).
47
48 51
52weakly_satisfiable_formula(1,(all(A,p(A))->some(B,(p(B),-p(f(B)))))).
53
54 57
58valid_formula(1,(all(x,(b(x)->c(x)))->all(x,b(x))->all(x,c(x)))).
59valid_formula(2,all(x,p==f(x))==(p==all(x,f(x)))).
60valid_formula(3,(all(z,some(y,all(x,f(x,y)==(f(x,z),-f(x,x)))))-> -some(z,all(x,f(x,z))))).
61valid_formula(4,all(y,f(y)==p)==(p==all(x,f(x)))).
62valid_formula(5,(f(1)==p)*(f(2)==p)==(p==f(1)*f(2))).
63valid_formula(6,all(A,p==f(A))==(p==all(B,f(B)))).
64valid_formula(7,(p==all(A,f(A)))==all(B,p==f(B))).
65valid_formula(8,(p==all(A,f(A))->all(B,(p->f(B))))).
66valid_formula(9,(p==all(A,f(A))->all(B,(f(B)->p)))).
67valid_formula(10,some(y,(all(x,f(x,y))->all(x,some(y,f(x,y)))))).
68valid_formula(11,(all(x,p(x))->some(z,all(y,p(y))))).
69valid_formula(12,some(x,some(y,(p(x,y)->all(x,all(y,p(x,y))))))).
70valid_formula(13,some(x,some(y,(p(x,y)->all(u,all(v,p(u,v))))))).
71valid_formula(14,(some(y,all(x,p(x,y)))->all(x,some(y,p(x,y))))).
72valid_formula(15,(all(A,p(A))-> -some(B,(p(B),-p(f(B)))))).
73valid_formula(16,a*b+a* -b+ -a*b+ -a* -b).
74valid_formula(17,(- -a->a)*(a-> - -a)).
75valid_formula(18,(a*b-> - (-a+ -b))*(- (-a+ -b)->a*b)).
76valid_formula(19,((-b->f)*(b*f-> -i)*(i+ -b-> -f)->b)).
77valid_formula(20,a+ -a).
78valid_formula(21,(((a->b)->a)->a)).
79valid_formula(22,(- -a->a)).
80valid_formula(23,(a->a)).
81valid_formula(24,(a->b->a)).
82valid_formula(25,((a->b)->(b->c)->a->c)).
83valid_formula(26,(a->(a->b)->b)).
84valid_formula(27,(a*(a->b)->b)).
85valid_formula(28,((a->b)-> -b-> -a)).
86valid_formula(29,(p->p;q->q)).
87valid_formula(30,(all(A,p(A))->all(y,p(y)))).
88valid_formula(31,(all(x,p(x))->some(y,p(y)))).
89valid_formula(32,all(x,p==f(x))==(p==all(x,f(x)))).
90valid_formula(33,(all(x,p==f(x))->p==all(x,f(x)))).
91valid_formula(34,(all(x,(p->f(x)))<-p==all(x,f(x)))).
92valid_formula(35,all(x,p==a(x))==(p==all(x,a(x)))).
93valid_formula(36,all(y,p==f(y))==(p==all(x,f(x)))).
94valid_formula(37,((p->all(x,f(x)))->all(x,(p->f(x))))).
95valid_formula(38,(p==all(x,f(x))->all(x,(f(x)->p)))).
96valid_formula(39,(all(x,(p<-f(x)))<-p==all(x,f(x)))).
97valid_formula(40,((p* -p->all(x,q(x)* -q(x)))->all(x,(q(x)* -q(x)->p* -p)))).
98valid_formula(41,((p->all(x,q(x)* -q(x)))->all(x,(q(x)* -q(x)->p)))).
99valid_formula(42,(p==all(x,f(x)))==all(x,p==f(x))).
100valid_formula(43,(p==q->(p->q),(q->p))).
101valid_formula(44,(p==q,r==q->p==r)).
102valid_formula(45,(some(A,p==f(A))->some(B,(f(B)->p)))).
103valid_formula(46,(some(A,p==f(A))->some(B,(f(B)->p)),some(C,(f(C)->p)))).
104valid_formula(47,(some(A,p==f(A))->some(B,(p->f(B)))->some(C,(f(C)->p)))).
105valid_formula(48,(some(A,p==f(A))->(-some(B,(p->f(B)));some(C,(f(C)->p))))).
106valid_formula(49,(and(some(A,p==f(A)),some(B,(p->f(B))))->some(C,(f(C)->p)))).
107valid_formula(50,(some(A,p==f(A))->some(B,(p->f(B))))).
108valid_formula(51,(some(A,p==f(A))->some(B,f(B)==p))).
109valid_formula(52,(all(x,p==f(x))->p==all(y,f(y)))).
110valid_formula(53,(p==all(x,f(x))->all(x,(p->f(x))))).
111valid_formula(54,(p==all(x,f(x))->all(x,(f(x)->p)))).
112valid_formula(55,all(x,p==f(x))==(p==all(y,f(y)))).
113valid_formula(56,(p==all(x,f(x))->all(x,p==f(x)))).
114valid_formula(57,(a->a)).
115valid_formula(58,(p==all(y,f(y))->all(x,(p->f(x))))).
116valid_formula(59,(all(A,p==f(A))<-all(B,f(B)==p))).
117valid_formula(60,(p==all(y,f(y))<-all(x,p==f(x)))).
118valid_formula(61,(p==all(y,f(y))->all(x,p==f(x)))).
119valid_formula(62,(p==all(y,f(y))->all(y,f(y)==p))).
120valid_formula(63,(p==all(y,f(y))->all(y,(f(y)->p)))).
121valid_formula(64,(p==all(x,f(x))->all(y,f(y)==p))).
122valid_formula(65,(p==all(x,f(x))->all(y,p==f(y)))).
123valid_formula(66,(p==all(y,f(y)))==all(x,p==f(x))).
124valid_formula(67,all(x,p)==p).
125valid_formula(68,some(x,p)==p).
126valid_formula(69,all(x,p(x))==all(y,p(y))).
127valid_formula(70,a*all(x,p(x))==all(x,a*p(x))).
128valid_formula(71,(a;all(x,p(x)))==all(x,(a;p(x)))).
129valid_formula(72,all(x,b(x))*all(x,c(x))==all(x,b(x)*c(x))).
130valid_formula(73,(some(x,b(x));some(x,c(x)))==some(x,(b(x);c(x)))).
131valid_formula(74,((all(x,b(x));all(x,c(x)))->all(x,(b(x);c(x))))).
132valid_formula(75,all(x,all(y,b(x,y)))==all(y,all(x,b(x,y)))).
133valid_formula(76,(some(x,all(y,b(x,y)))->all(y,some(x,b(x,y))))).
134valid_formula(77,some(x,all(y,b(x,y)))==all(y,some(x,b(x,y)))).
135valid_formula(78,(all(x,b(x))->some(y,b(y)))).
136valid_formula(79,-all(x,b(x))==some(x,-b(x))).
137valid_formula(80,-some(x,b(x))==all(x,-b(x))).
138valid_formula(81,(a->all(x,b(x)))==all(x,(a->b(x)))).
139valid_formula(82,(a->some(x,b(x)))==some(x,(a->b(x)))).
140valid_formula(83,(all(x,b(x))->a)==some(x,(b(x)->a))).
141valid_formula(84,(some(x,b(x))->a)==all(x,(b(x)->a))).
142valid_formula(85,(all(x,(b(x)->c(x)))->some(x,b(x))->some(x,c(x)))).
143valid_formula(86,all(x,(p(x)->q(x)->p(x)))).
144valid_formula(87,all(x,(p(x)->p(x)))).
145valid_formula(88,(all(x,all(y,p(x,y)))->some(x,some(y,p(x,y))))).
146valid_formula(89,-some(x,all(y,f(y,x)== -f(y,y)))).
147valid_formula(90,(b==a->(a->b)*(b->a))).
148valid_formula(91,(b==a)==(a==b)).
149valid_formula(92,(all(x,(b(x)->c(x)))->all(x,b(x))->all(x,c(x)))).
150
151 154
155invalid_formula(1,(some(x,b(x))*some(x,c(x))->some(x,b(x)*c(x)))).
156invalid_formula(2,((all(x,b(x));all(x,c(x)))<-all(x,(b(x);c(x))))).
157invalid_formula(3,(all(A,some(B,p(A,B)))->some(B,all(A,p(A,B))))).
158invalid_formula(4,- (all(A,p(A))->some(B,(p(B),-p(f(B)))))).
159invalid_formula(5,(all(x,some(p(x,y)))->some(y,all(x,p(x,y))))).
160invalid_formula(6,a).
161invalid_formula(7,((a->b)->a)).
162invalid_formula(8,((a->b)->b->a)).
163invalid_formula(9,(a->b->c)).
164invalid_formula(10,(all(x,(p<-f(x)))<-p<-all(x,f(x)))).
165invalid_formula(11,((p->all(x,f(x)))->all(x,(f(x)->p)))).
166invalid_formula(12,(- (p->all(x,f(x)));all(x,(f(x)->p)))).
167invalid_formula(13,(- (-p;all(x,f(x)));all(x,(f(x)->p)))).
168invalid_formula(14,(p*some(x,-f(x));all(x,(-f(x)|p)))).
169invalid_formula(15,(p*some(x,-f(x));all(x,-f(x)))).
170invalid_formula(16,(p* -f(a);all(x,-f(x)))).
171invalid_formula(17,((p->q)->p)).
172invalid_formula(18,- ((-b->f)*(b*f-> -i)*(i+ -b-> -f)->i*f)).
173
174
175
176
177 180
181unsatisfiable_formula(1,all(x,p==f(x))==(p->all(y,f(y)))).
182unsatisfiable_formula(2,some(x,(b(x)->c(x)))==(all(x,b(x))->all(x,c(x)))).
183unsatisfiable_formula(3,(some(x,p(x))->all(y,p(y)))).
184unsatisfiable_formula(4,all(y,(some(x,f(x,y))->some(x,all(y,f(x,y)))))).
185unsatisfiable_formula(5,(some(A,p(A))->all(A,p(A)))).
186unsatisfiable_formula(6,(some(x,p(x))->all(y,p(y)))).
187unsatisfiable_formula(7,all(y,(some(x,f(x,y))->some(x,all(y,f(x,y)))))).
188unsatisfiable_formula(8,(some(A,p(A))->all(A,p(A)))).
189unsatisfiable_formula(9,(some(x,b(x))->all(y,b(y)))).
190unsatisfiable_formula(10,all(x,p==f(x))==(p->all(y,f(y)))).
191unsatisfiable_formula(11,- ((-b->f)*(b*f-> -i)*(i+ -b-> -f)->b)).
192unsatisfiable_formula(12,(some(x,b(x))->all(y,b(y)))).
193unsatisfiable_formula(13,(some(A,p(A))->all(A,p(A)))).
194unsatisfiable_formula(14,all(y,(some(x,f(x,y))->some(x,all(y,f(x,y)))))).
195unsatisfiable_formula(15,(some(x,p(x))->all(y,p(y)))).
196unsatisfiable_formula(16,some(x,(b(x)->c(x)))==(all(x,b(x))->all(x,c(x)))).
197unsatisfiable_formula(17,(some(x,p(x))->all(y,p(y)))).
198unsatisfiable_formula(18,all(y,(some(x,f(x,y))->some(x,all(y,f(x,y)))))).
199unsatisfiable_formula(19,(some(A,p(A))->all(A,p(A))))