testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
98   1,716   50   1.96
0   1,242   0.51   50
50     1  
1    
 
  CalculateTruthTestCase       Line # 27 98 50 100% 1.0
 
  (184)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.logic.model;
17   
18    import org.qedeq.kernel.bo.test.QedeqBoTestCase;
19    import org.qedeq.kernel.se.base.list.Element;
20    import org.qedeq.kernel.xml.parser.BasicParser;
21   
22    /**
23    * For testing {@link org.qedeq.kernel.bo.logic.model.CalculateTruth}.
24    *
25    * @author Michael Meyling
26    */
 
27    public abstract class CalculateTruthTestCase extends QedeqBoTestCase {
28   
29    /** Model to use. */
30    private Model model;
31   
32   
33    /**
34    * Constructor.
35    *
36    * @param model Model to use.
37    */
 
38  189 toggle public CalculateTruthTestCase(final Model model) {
39  189 super();
40  189 this.model = model;
41    }
42   
43    /**
44    * Get model we use here.
45    *
46    * @return Model.
47    */
 
48  189 toggle public Model getModel() {
49  189 return model;
50    }
51   
52    /**
53    * Check if given formula is a tautology.
54    *
55    * @param fomula Formula to check.
56    * @return Check successful?
57    * @throws HeuristicException
58    */
 
59  141 toggle protected boolean isTautology(final Element fomula) throws HeuristicException {
60  141 Test failure here return CalculateTruth.isTautology(getModel(), fomula);
61    }
62   
63    /**
64    * Function: isTautology(Element)
65    * Type: negative
66    * Data: --A
67    *
68    * @throws Exception Test failed.
69    */
 
70  4 toggle public void testTautology01() throws Exception {
71  4 final Element ele = BasicParser.createElement(
72    "<NOT><NOT><PREDVAR id=\"A\"/></NOT></NOT>");
73    // System.out.println(ele.toString());
74  4 assertFalse(isTautology(ele));
75    }
76   
77    /**
78    * Function: isTautology(Element)
79    * Type: positive
80    * Data: A v -A
81    *
82    * @throws Exception Test failed.
83    */
 
84  4 toggle public void testTautology02() throws Exception {
85  4 final Element ele = BasicParser.createElement(
86    "<OR><PREDVAR id=\"A\"/><NOT><PREDVAR id=\"A\"/></NOT></OR>");
87    // System.out.println(ele.toString());
88  4 assertTrue(isTautology(ele));
89    }
90   
91    /**
92    * Function: isTautology(Element)
93    * Type: negative
94    * Data: A n -A
95    *
96    * @throws Exception Test failed.
97    */
 
98  4 toggle public void testTautology03() throws Exception {
99  4 final Element ele = BasicParser.createElement(
100    "<AND><PREDVAR id=\"A\"/><NOT><PREDVAR id=\"A\"/></NOT></AND>");
101    // System.out.println(ele.toString());
102  4 assertFalse(isTautology(ele));
103    }
104   
105    /**
106    * Function: isTautology(Element)
107    * Type: negative
108    * Data: A => -A
109    *
110    * @throws Exception Test failed.
111    */
 
112  4 toggle public void testTautology04() throws Exception {
113  4 final Element ele = BasicParser.createElement(
114    "<IMPL><PREDVAR id=\"A\"/><NOT><PREDVAR id=\"A\"/></NOT></IMPL>");
115    // System.out.println(ele.toString());
116  4 assertFalse(isTautology(ele));
117    }
118   
119    /**
120    * Function: isTautology(Element)
121    * Type: negative
122    * Data: -A => A
123    *
124    * @throws Exception Test failed.
125    */
 
126  4 toggle public void testTautology05() throws Exception {
127  4 final Element ele = BasicParser.createElement(
128    "<IMPL><NOT><PREDVAR id=\"A\"/></NOT><PREDVAR id=\"A\"/></IMPL>");
129    // System.out.println(ele.toString());
130  4 assertFalse(isTautology(ele));
131    }
132   
133    /**
134    * Function: isTautology(Element)
135    * Type: positive
136    * Data: A => A
137    *
138    * @throws Exception Test failed.
139    */
 
140  4 toggle public void testTautology06() throws Exception {
141  4 final Element ele = BasicParser.createElement(
142    "<IMPL><PREDVAR id=\"A\"/><PREDVAR id=\"A\"/></IMPL>");
143    // System.out.println(ele.toString());
144  4 assertTrue(isTautology(ele));
145    }
146   
147    /**
148    * Function: isTautology(Element)
149    * Type: positive
150    * Data: A -> A
151    *
152    * @throws Exception Test failed.
153    */
 
154  4 toggle public void testTautology07() throws Exception {
155  4 final Element ele = BasicParser.createElement(
156    "<IMPL><PREDVAR id=\"A\"/><NOT><NOT><PREDVAR id=\"A\"/></NOT></NOT></IMPL>");
157    // System.out.println(ele.toString());
158  4 assertTrue(isTautology(ele));
159    }
160   
161    /**
162    * Function: isTautology(Element)
163    * Type: positive
164    * Data: A <-> A
165    *
166    * @throws Exception Test failed.
167    */
 
168  4 toggle public void testTautology08() throws Exception {
169  4 final Element ele = BasicParser.createElement(
170    "<EQUI><PREDVAR id=\"A\"/><NOT><NOT><PREDVAR id=\"A\"/></NOT></NOT></EQUI>");
171    // System.out.println(ele.toString());
172  4 assertTrue(isTautology(ele));
173    }
174   
175    /**
176    * Function: isTautology(Element)
177    * Type: positive
178    * Data: A -> B v A
179    *
180    * @throws Exception Test failed.
181    */
 
182  4 toggle public void testTautology09() throws Exception {
183  4 final Element ele = BasicParser.createElement(
184    "<IMPL><PREDVAR id=\"A\"/><OR><PREDVAR id=\"B\"/><PREDVAR id=\"A\"/></OR></IMPL>");
185    // System.out.println(ele.toString());
186  4 assertTrue(isTautology(ele));
187    }
188   
189    /**
190    * Function: isTautology(Element)
191    * Type: positive
192    * Data: A -> -B v A
193    *
194    * @throws Exception Test failed.
195    */
 
196  4 toggle public void testTautology10() throws Exception {
197  4 final Element ele = BasicParser.createElement(
198    "<IMPL><PREDVAR id=\"A\"/><OR><NOT><PREDVAR id=\"B\"/></NOT><PREDVAR id=\"A\"/></OR></IMPL>");
199    // System.out.println(ele.toString());
200  4 assertTrue(isTautology(ele));
201    }
202   
203    /**
204    * Function: isTautology(Element)
205    * Type: negative
206    * Data: A -> -B n A
207    *
208    * @throws Exception Test failed.
209    */
 
210  4 toggle public void testTautology11() throws Exception {
211  4 final Element ele = BasicParser.createElement(
212    "<IMPL><PREDVAR id=\"A\"/><AND><NOT><PREDVAR id=\"B\"/></NOT><PREDVAR id=\"A\"/></AND></IMPL>");
213    // System.out.println(ele.toString());
214  4 assertFalse(isTautology(ele));
215    }
216   
217    /**
218    * Function: isTautology(Element)
219    * Type: positive
220    * Data: A -> A v -A
221    *
222    * @throws Exception Test failed.
223    */
 
224  4 toggle public void testTautology12() throws Exception {
225  4 final Element ele = BasicParser.createElement(
226    "<IMPL><PREDVAR id=\"A\"/><OR><PREDVAR id=\"A\"/><NOT><PREDVAR id=\"A\"/></NOT></OR></IMPL>");
227    // System.out.println(ele.toString());
228  4 assertTrue(isTautology(ele));
229    }
230   
231    /**
232    * Function: isTautology(Element)
233    * Type: positive
234    * Data: A -> A v B v C v D v E v F v G v H v I v J
235    *
236    * @throws Exception Test failed.
237    */
 
238  4 toggle public void testTautology13() throws Exception {
239  4 final Element ele = BasicParser.createElement(
240    "<IMPL><PREDVAR id=\"A\"/><OR><PREDVAR id=\"A\"/><PREDVAR id=\"B\"/><PREDVAR id=\"C\"/>"
241    + "<PREDVAR id=\"D\"/><PREDVAR id=\"E\"/><PREDVAR id=\"F\"/><PREDVAR id=\"G\"/>"
242    + "<PREDVAR id=\"H\"/><PREDVAR id=\"I\"/><PREDVAR id=\"J\"/></OR></IMPL>");
243    // System.out.println(ele.toString());
244  4 assertTrue(isTautology(ele));
245    }
246   
247    /**
248    * Function: isTautology(Element)
249    * Type: positive
250    * Data: A v B <-> B v A
251    *
252    * @throws Exception Test failed.
253    */
 
254  4 toggle public void testTautology14() throws Exception {
255  4 final Element ele = BasicParser.createElement(
256    "<EQUI><OR><PREDVAR id=\"A\"/><PREDVAR id=\"B\"/></OR>"
257    + "<OR><PREDVAR id=\"B\"/><PREDVAR id=\"A\"/></OR></EQUI>");
258    // System.out.println(ele.toString());
259  4 assertTrue(isTautology(ele));
260    }
261   
262    /**
263    * Function: isTautology(Element)
264    * Type: positive
265    * Data: A n B <-> B n A
266    *
267    * @throws Exception Test failed.
268    */
 
269  4 toggle public void testTautology15() throws Exception {
270  4 final Element ele = BasicParser.createElement(
271    "<EQUI><AND><PREDVAR id=\"A\"/><PREDVAR id=\"B\"/></AND>"
272    + "<AND><PREDVAR id=\"B\"/><PREDVAR id=\"A\"/></AND></EQUI>");
273    // System.out.println(ele.toString());
274  4 assertTrue(isTautology(ele));
275    }
276   
277    /**
278    * Function: isTautology(Element)
279    * Type: negative
280    * Data: A n B <-> B v A
281    *
282    * @throws Exception Test failed.
283    */
 
284  4 toggle public void testTautology16() throws Exception {
285  4 final Element ele = BasicParser.createElement(
286    "<EQUI><AND><PREDVAR id=\"A\"/><PREDVAR id=\"B\"/></AND>"
287    + "<OR><PREDVAR id=\"B\"/><PREDVAR id=\"A\"/></OR></EQUI>");
288    // System.out.println(ele.toString());
289  4 assertFalse(isTautology(ele));
290    }
291   
292    /**
293    * Function: isTautology(Element)
294    * Type: positive
295    * Data: -A n B <-> -(-B v A)
296    *
297    * @throws Exception Test failed.
298    */
 
299  4 toggle public void testTautology17() throws Exception {
300  4 final Element ele = BasicParser.createElement(
301    "<EQUI><AND><NOT><PREDVAR id=\"A\"/></NOT><PREDVAR id=\"B\"/></AND>"
302    + "<NOT><OR><NOT><PREDVAR id=\"B\"/></NOT><PREDVAR id=\"A\"/></OR></NOT></EQUI>");
303    // System.out.println(ele.toString());
304  4 assertTrue(isTautology(ele));
305    }
306   
307    /**
308    * Function: isTautology(Element)
309    * Type: positive
310    * Data: A(x,y) <-> A(x,y)
311    *
312    * @throws Exception Test failed.
313    */
 
314  4 toggle public void testTautology18() throws Exception {
315  4 final Element ele = BasicParser.createElement(
316    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
317    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR></EQUI>");
318    // System.out.println(ele.toString());
319  4 assertTrue(isTautology(ele));
320    }
321   
322    /**
323    * Function: isTautology(Element)
324    * Type: negative
325    * Data: A(x,y) <-> A(y,x)
326    *
327    * @throws Exception Test failed.
328    */
 
329  2 toggle public void testTautology19() throws Exception {
330  2 final Element ele = BasicParser.createElement(
331    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
332    + "<PREDVAR id=\"A\"><VAR id=\"y\"/><VAR id=\"x\"/></PREDVAR></EQUI>");
333    // System.out.println(ele.toString());
334  2 assertFalse(isTautology(ele));
335    }
336   
337    /**
338    * Function: isTautology(Element)
339    * Type: negative
340    * Data: A(x,y) <-> A(x,x)
341    *
342    * @throws Exception Test failed.
343    */
 
344  2 toggle public void testTautology20() throws Exception {
345  2 final Element ele = BasicParser.createElement(
346    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
347    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"x\"/></PREDVAR></EQUI>");
348    // System.out.println(ele.toString());
349  2 assertFalse(isTautology(ele));
350    }
351   
352    /**
353    * Function: isTautology(Element)
354    * Type: negative
355    * Data: A(y) <-> A(x)
356    *
357    * @throws Exception Test failed.
358    */
 
359  2 toggle public void testTautology21() throws Exception {
360  2 final Element ele = BasicParser.createElement(
361    "<EQUI><PREDVAR id=\"A\"><VAR id=\"y\"/></PREDVAR>"
362    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></EQUI>");
363    // System.out.println(ele.toString());
364  2 assertFalse(isTautology(ele));
365    }
366   
367    /**
368    * Function: isTautology(Element)
369    * Type: negative
370    * Data: A(x, y) <-> A(x)
371    *
372    * @throws Exception Test failed.
373    */
 
374  4 toggle public void testTautology22() throws Exception {
375  4 final Element ele = BasicParser.createElement(
376    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
377    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></EQUI>");
378    // System.out.println(ele.toString());
379  4 assertFalse(isTautology(ele));
380    }
381   
382    /**
383    * Function: isTautology(Element)
384    * Type: negative
385    * Data: A <-> A(x)
386    *
387    * @throws Exception Test failed.
388    */
 
389  4 toggle public void testTautology23() throws Exception {
390  4 final Element ele = BasicParser.createElement(
391    "<EQUI><PREDVAR id=\"A\"/>"
392    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></EQUI>");
393    // System.out.println(ele.toString());
394  4 assertFalse(isTautology(ele));
395    }
396   
397    /**
398    * Function: isTautology(Element)
399    * Type: negative
400    * Data: A <-> B
401    *
402    * @throws Exception Test failed.
403    */
 
404  4 toggle public void testTautology24() throws Exception {
405  4 final Element ele = BasicParser.createElement(
406    "<EQUI><PREDVAR id=\"A\"/>"
407    + "<PREDVAR id=\"B\"/></EQUI>");
408    // System.out.println(ele.toString());
409  4 assertFalse(isTautology(ele));
410    }
411   
412    /**
413    * Function: isTautology(Element)
414    * Type: negative
415    * Data: A -> B
416    *
417    * @throws Exception Test failed.
418    */
 
419  4 toggle public void testTautology25() throws Exception {
420  4 final Element ele = BasicParser.createElement(
421    "<IMPL><PREDVAR id=\"A\"/>"
422    + "<PREDVAR id=\"B\"/></IMPL>");
423    // System.out.println(ele.toString());
424  4 assertFalse(isTautology(ele));
425    }
426   
427    /**
428    * Function: isTautology(Element)
429    * Type: negative
430    * Data: A -> A(x)
431    *
432    * @throws Exception Test failed.
433    */
 
434  4 toggle public void testTautology26() throws Exception {
435  4 final Element ele = BasicParser.createElement(
436    "<IMPL><PREDVAR id=\"A\"/>"
437    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></IMPL>");
438    // System.out.println(ele.toString());
439  4 assertFalse(isTautology(ele));
440    }
441   
442    /**
443    * Function: isTautology(Element)
444    * Type: positive
445    * Data: \forall x (A(x) -> A(x))
446    *
447    * @throws Exception Test failed.
448    */
 
449  4 toggle public void testTautology27() throws Exception {
450  4 final Element ele = BasicParser.createElement(
451    "<FORALL><VAR id=\"x\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR>"
452    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></IMPL></FORALL>");
453    // System.out.println(ele.toString());
454  4 assertTrue(isTautology(ele));
455    }
456   
457    /**
458    * Function: isTautology(Element)
459    * Type: negative
460    * Data: \forall x \forall y (A(x) -> A(y))
461    *
462    * @throws Exception Test failed.
463    */
 
464  2 toggle public void testTautology28() throws Exception {
465  2 final Element ele = BasicParser.createElement(
466    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR>"
467    + "<PREDVAR id=\"A\"><VAR id=\"y\"/></PREDVAR></IMPL></FORALL></FORALL>");
468    // System.out.println(ele.toString());
469  2 assertFalse(isTautology(ele));
470    }
471   
472    /**
473    * Function: isTautology(Element)
474    * Type: positive
475    * Data: \forall x \forall y (A(x,y) -> A(x,y))
476    *
477    * @throws Exception Test failed.
478    */
 
479  4 toggle public void testTautology29() throws Exception {
480  4 final Element ele = BasicParser.createElement(
481    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
482    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR></IMPL></FORALL></FORALL>");
483    // System.out.println(ele.toString());
484  4 assertTrue(isTautology(ele));
485    }
486   
487    /**
488    * Function: isTautology(Element)
489    * Type: positive
490    * Data: \forall x \forall A(x,y): A(x,y))
491    *
492    * @throws Exception Test failed.
493    */
 
494  4 toggle public void testTautology30() throws Exception {
495  4 final Element ele = BasicParser.createElement(
496    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
497    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR></FORALL></FORALL>");
498    // System.out.println(ele.toString());
499  4 assertTrue(isTautology(ele));
500    }
501   
502    /**
503    * Function: isTautology(Element)
504    * Type: negative
505    * Data: \forall x \forall A(x,y): A(y,x))
506    *
507    * @throws Exception Test failed.
508    */
 
509  2 toggle public void testTautology31() throws Exception {
510  2 final Element ele = BasicParser.createElement(
511    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
512    + "<PREDVAR id=\"A\"><VAR id=\"y\"/><VAR id=\"x\"/></PREDVAR></FORALL></FORALL>");
513    // System.out.println(ele.toString());
514  2 assertFalse(isTautology(ele));
515    }
516   
517    /**
518    * Function: isTautology(Element)
519    * Type: positive
520    * Data: \forall x \exists y (A(x) -> A(y))
521    *
522    * @throws Exception Test failed.
523    */
 
524  4 toggle public void testTautology32() throws Exception {
525  4 final Element ele = BasicParser.createElement(
526    "<FORALL><VAR id=\"x\"/><EXISTS><VAR id=\"y\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR>"
527    + "<PREDVAR id=\"A\"><VAR id=\"y\"/></PREDVAR></IMPL></EXISTS></FORALL>");
528    // System.out.println(ele.toString());
529  4 assertTrue(isTautology(ele));
530    }
531   
532    /**
533    * Function: isTautology(Element)
534    * Type: positive
535    * Data: \exists! y (x = y)
536    *
537    * @throws Exception Test failed.
538    */
 
539  4 toggle public void testTautology33() throws Exception {
540  4 final Element ele = BasicParser.createElement(
541    "<EXISTSU><VAR id=\"y\"/><PREDCON id=\"equal\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDCON>"
542    + "</EXISTSU>");
543    // System.out.println(ele.toString());
544  4 assertTrue(isTautology(ele));
545    }
546   
547    /**
548    * Function: isTautology(Element)
549    * Type: negative
550    * Data: \exists! y (y = y)
551    *
552    * @throws Exception Test failed.
553    */
 
554  2 toggle public void testTautology34() throws Exception {
555  2 final Element ele = BasicParser.createElement(
556    "<EXISTSU><VAR id=\"y\"/><PREDCON id=\"equal\"><VAR id=\"y\"/><VAR id=\"y\"/></PREDCON>"
557    + "</EXISTSU>");
558    // System.out.println(ele.toString());
559  2 assertFalse(isTautology(ele));
560    }
561   
562    /**
563    * Function: isTautology(Element)
564    * Type: positive
565    * Data: \exists y (y = y)
566    *
567    * @throws Exception Test failed.
568    */
 
569  4 toggle public void testTautology35() throws Exception {
570  4 final Element ele = BasicParser.createElement(
571    "<EXISTS><VAR id=\"y\"/><PREDCON id=\"equal\"><VAR id=\"y\"/><VAR id=\"y\"/></PREDCON>"
572    + "</EXISTS>");
573    // System.out.println(ele.toString());
574  4 assertTrue(isTautology(ele));
575    }
576   
577    /**
578    * Function: isTautology(Element)
579    * Type: positive
580    * Data: f(y) = f(y)
581    *
582    * @throws Exception Test failed.
583    */
 
584  4 toggle public void testTautology36() throws Exception {
585  4 final Element ele = BasicParser.createElement(
586    "<PREDCON id=\"equal\"><FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR>"
587    + "<FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR></PREDCON>");
588    // System.out.println(ele.toString());
589  4 assertTrue(isTautology(ele));
590    }
591   
592    /**
593    * Function: isTautology(Element)
594    * Type: negative
595    * Data: f(x) = f(y)
596    *
597    * @throws Exception Test failed.
598    */
 
599  2 toggle public void testTautology37() throws Exception {
600  2 final Element ele = BasicParser.createElement(
601    "<PREDCON id=\"equal\"><FUNVAR id=\"f\"><VAR id=\"x\"/></FUNVAR>"
602    + "<FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR></PREDCON>");
603    // System.out.println(ele.toString());
604  2 assertFalse(isTautology(ele));
605    }
606   
607    /**
608    * Function: isTautology(Element)
609    * Type: negative
610    * Data: \exists y f(x) = f(y)
611    *
612    * @throws Exception Test failed.
613    */
 
614  4 toggle public void testTautology38() throws Exception {
615  4 final Element ele = BasicParser.createElement(
616    "<EXISTS><VAR id=\"y\"/><PREDCON id=\"equal\"><FUNVAR id=\"f\"><VAR id=\"x\"/></FUNVAR>"
617    + "<FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR></PREDCON></EXISTS>");
618    // System.out.println(ele.toString());
619  4 assertTrue(isTautology(ele));
620    }
621   
622    /**
623    * Function: isTautology(Element)
624    * Type: positive
625    * Data: see qedeq_logic_v1.xml theorem:propositionalCalculus from 2010-09-26
626    *
627    * @throws Exception Test failed.
628    */
 
629  4 toggle public void testTautology39() throws Exception {
630  4 final Element ele = BasicParser.createElement(
631    "\n <AND>\n" +
632    "\n" +
633    "\n <PREDCON ref=\"TRUE\" />\n" +
634    "\n" +
635    "\n <NOT>\n" +
636    "\n <PREDCON ref=\"FALSE\" />\n" +
637    "\n </NOT>" +
638    "\n" +
639    "\n <IMPL>" +
640    "\n <PREDVAR id=\"A\" />" +
641    "\n <PREDVAR id=\"A\" />" +
642    "\n </IMPL>" +
643    "\n" +
644    "\n <EQUI>" +
645    "\n <PREDVAR id=\"A\" />" +
646    "\n <PREDVAR id=\"A\" />" +
647    "\n </EQUI>" +
648    "\n" +
649    "\n <EQUI>" +
650    "\n <OR>" +
651    "\n <PREDVAR id=\"A\" />" +
652    "\n <PREDVAR id=\"B\" />" +
653    "\n </OR>" +
654    "\n <OR>" +
655    "\n <PREDVAR id=\"B\" />" +
656    "\n <PREDVAR id=\"A\" />" +
657    "\n </OR>" +
658    "\n </EQUI>" +
659    "\n" +
660    "\n <EQUI>" +
661    "\n <AND>" +
662    "\n <PREDVAR id=\"A\" />" +
663    "\n <PREDVAR id=\"B\" />" +
664    "\n </AND>" +
665    "\n <AND>" +
666    "\n <PREDVAR id=\"B\" />" +
667    "\n <PREDVAR id=\"A\" />" +
668    "\n </AND>" +
669    "\n </EQUI>" +
670    "\n" +
671    "\n <IMPL>" +
672    "\n <AND>" +
673    "\n <PREDVAR id=\"A\" />" +
674    "\n <PREDVAR id=\"B\" />" +
675    "\n </AND>" +
676    "\n <PREDVAR id=\"A\" />" +
677    "\n </IMPL>" +
678    "\n" +
679    "\n <EQUI>" +
680    "\n <EQUI>" +
681    "\n <PREDVAR id=\"A\" />" +
682    "\n <PREDVAR id=\"B\" />" +
683    "\n </EQUI>" +
684    "\n <EQUI>" +
685    "\n <PREDVAR id=\"B\" />" +
686    "\n <PREDVAR id=\"A\" />" +
687    "\n </EQUI>" +
688    "\n </EQUI>" +
689    "\n" +
690    "\n <EQUI>" +
691    "\n <OR>" +
692    "\n <PREDVAR id=\"A\" />" +
693    "\n <OR>" +
694    "\n <PREDVAR id=\"B\" />" +
695    "\n <PREDVAR id=\"C\" />" +
696    "\n </OR>" +
697    "\n </OR>" +
698    "\n <OR>" +
699    "\n <OR>" +
700    "\n <PREDVAR id=\"A\" />" +
701    "\n <PREDVAR id=\"B\" />" +
702    "\n </OR>" +
703    "\n <PREDVAR id=\"C\" />" +
704    "\n </OR>" +
705    "\n </EQUI>" +
706    "\n" +
707    "\n <EQUI>" +
708    "\n <AND>" +
709    "\n <PREDVAR id=\"A\" />" +
710    "\n <AND>" +
711    "\n <PREDVAR id=\"B\" />" +
712    "\n <PREDVAR id=\"C\" />" +
713    "\n </AND>" +
714    "\n </AND>" +
715    "\n <AND>" +
716    "\n <AND>" +
717    "\n <PREDVAR id=\"A\" />" +
718    "\n <PREDVAR id=\"B\" />" +
719    "\n </AND>" +
720    "\n <PREDVAR id=\"C\" />" +
721    "\n </AND>" +
722    "\n </EQUI>" +
723    "\n" +
724    "\n <EQUI>" +
725    "\n <PREDVAR id=\"A\" />" +
726    "\n <OR>" +
727    "\n <PREDVAR id=\"A\" />" +
728    "\n <PREDVAR id=\"A\" />" +
729    "\n </OR>" +
730    "\n </EQUI>" +
731    "\n" +
732    "\n <EQUI>" +
733    "\n <PREDVAR id=\"A\" />" +
734    "\n <AND>" +
735    "\n <PREDVAR id=\"A\" />" +
736    "\n <PREDVAR id=\"A\" />" +
737    "\n </AND>" +
738    "\n </EQUI>" +
739    "\n" +
740    "\n <EQUI>" +
741    "\n <PREDVAR id=\"A\" />" +
742    "\n <NOT>" +
743    "\n <NOT>" +
744    "\n <PREDVAR id=\"A\" />" +
745    "\n </NOT>" +
746    "\n </NOT>" +
747    "\n </EQUI>" +
748    "\n" +
749    "\n <EQUI>" +
750    "\n <IMPL>" +
751    "\n <PREDVAR id=\"A\" />" +
752    "\n <PREDVAR id=\"B\" />" +
753    "\n </IMPL>" +
754    "\n <IMPL>" +
755    "\n <NOT>" +
756    "\n <PREDVAR id=\"B\" />" +
757    "\n </NOT>" +
758    "\n <NOT>" +
759    "\n <PREDVAR id=\"A\" />" +
760    "\n </NOT>" +
761    "\n </IMPL>" +
762    "\n </EQUI>" +
763    "\n" +
764    "\n <EQUI>" +
765    "\n <EQUI>" +
766    "\n <PREDVAR id=\"A\" />" +
767    "\n <PREDVAR id=\"B\" />" +
768    "\n </EQUI>" +
769    "\n <EQUI>" +
770    "\n <NOT>" +
771    "\n <PREDVAR id=\"A\" />" +
772    "\n </NOT>" +
773    "\n <NOT>" +
774    "\n <PREDVAR id=\"B\" />" +
775    "\n </NOT>" +
776    "\n </EQUI>" +
777    "\n </EQUI>" +
778    "\n" +
779    "\n <EQUI>" +
780    "\n <IMPL>" +
781    "\n <PREDVAR id=\"A\" />" +
782    "\n <IMPL>" +
783    "\n <PREDVAR id=\"B\" />" +
784    "\n <PREDVAR id=\"C\" />" +
785    "\n </IMPL>" +
786    "\n </IMPL>" +
787    "\n <IMPL>" +
788    "\n <PREDVAR id=\"B\" />" +
789    "\n <IMPL>" +
790    "\n <PREDVAR id=\"A\" />" +
791    "\n <PREDVAR id=\"C\" />" +
792    "\n </IMPL>" +
793    "\n </IMPL>" +
794    "\n </EQUI>" +
795    "\n" +
796    "\n <EQUI>" +
797    "\n <NOT>" +
798    "\n <OR>" +
799    "\n <PREDVAR id=\"A\" />" +
800    "\n <PREDVAR id=\"B\" />" +
801    "\n </OR>" +
802    "\n </NOT>" +
803    "\n <AND>" +
804    "\n <NOT>" +
805    "\n <PREDVAR id=\"A\" />" +
806    "\n </NOT>" +
807    "\n <NOT>" +
808    "\n <PREDVAR id=\"B\" />" +
809    "\n </NOT>" +
810    "\n </AND>" +
811    "\n </EQUI>" +
812    "\n" +
813    "\n <EQUI>" +
814    "\n <NOT>" +
815    "\n <AND>" +
816    "\n <PREDVAR id=\"A\" />" +
817    "\n <PREDVAR id=\"B\" />" +
818    "\n </AND>" +
819    "\n </NOT>" +
820    "\n <OR>" +
821    "\n <NOT>" +
822    "\n <PREDVAR id=\"A\" />" +
823    "\n </NOT>" +
824    "\n <NOT>" +
825    "\n <PREDVAR id=\"B\" />" +
826    "\n </NOT>" +
827    "\n </OR>" +
828    "\n </EQUI>" +
829    "\n" +
830    "\n <EQUI>" +
831    "\n <OR>" +
832    "\n <PREDVAR id=\"A\" />" +
833    "\n <AND>" +
834    "\n <PREDVAR id=\"B\" />" +
835    "\n <PREDVAR id=\"C\" />" +
836    "\n </AND>" +
837    "\n </OR>" +
838    "\n <AND>" +
839    "\n <OR>" +
840    "\n <PREDVAR id=\"A\" />" +
841    "\n <PREDVAR id=\"B\" />" +
842    "\n </OR>" +
843    "\n <OR>" +
844    "\n <PREDVAR id=\"A\" />" +
845    "\n <PREDVAR id=\"C\" />" +
846    "\n </OR>" +
847    "\n </AND>" +
848    "\n </EQUI>" +
849    "\n" +
850    "\n <EQUI>" +
851    "\n <AND>" +
852    "\n <PREDVAR id=\"A\" />" +
853    "\n <OR>" +
854    "\n <PREDVAR id=\"B\" />" +
855    "\n <PREDVAR id=\"C\" />" +
856    "\n </OR>" +
857    "\n </AND>" +
858    "\n <OR>" +
859    "\n <AND>" +
860    "\n <PREDVAR id=\"A\" />" +
861    "\n <PREDVAR id=\"B\" />" +
862    "\n </AND>" +
863    "\n <AND>" +
864    "\n <PREDVAR id=\"A\" />" +
865    "\n <PREDVAR id=\"C\" />" +
866    "\n </AND>" +
867    "\n </OR>" +
868    "\n </EQUI>" +
869    "\n" +
870    "\n <EQUI>" +
871    "\n <AND>" +
872    "\n <PREDVAR id=\"A\" />" +
873    "\n <PREDCON ref=\"TRUE\" />" +
874    "\n </AND>" +
875    "\n <PREDVAR id=\"A\" />" +
876    "\n </EQUI>" +
877    "\n" +
878    "\n <EQUI>" +
879    "\n <AND>" +
880    "\n <PREDVAR id=\"A\" />" +
881    "\n <PREDCON ref=\"FALSE\" />" +
882    "\n </AND>" +
883    "\n <PREDCON ref=\"FALSE\" />" +
884    "\n </EQUI>" +
885    "\n" +
886    "\n <EQUI>" +
887    "\n <OR>" +
888    "\n <PREDVAR id=\"A\" />" +
889    "\n <PREDCON ref=\"TRUE\" />" +
890    "\n </OR>" +
891    "\n <PREDCON ref=\"TRUE\" />" +
892    "\n </EQUI>" +
893    "\n" +
894    "\n <EQUI>" +
895    "\n <OR>" +
896    "\n <PREDVAR id=\"A\" />" +
897    "\n <PREDCON ref=\"FALSE\" />" +
898    "\n </OR>" +
899    "\n <PREDVAR id=\"A\" />" +
900    "\n </EQUI>" +
901    "\n" +
902    "\n <EQUI>" +
903    "\n <OR>" +
904    "\n <PREDVAR id=\"A\" />" +
905    "\n <NOT>" +
906    "\n <PREDVAR id=\"A\" />" +
907    "\n </NOT>" +
908    "\n </OR>" +
909    "\n <PREDCON ref=\"TRUE\" />" +
910    "\n </EQUI>" +
911    "\n" +
912    "\n <EQUI>" +
913    "\n <AND>" +
914    "\n <PREDVAR id=\"A\" />" +
915    "\n <NOT>" +
916    "\n <PREDVAR id=\"A\" />" +
917    "\n </NOT>" +
918    "\n </AND>" +
919    "\n <PREDCON ref=\"FALSE\" />" +
920    "\n </EQUI>" +
921    "\n" +
922    "\n <EQUI>" +
923    "\n <IMPL>" +
924    "\n <PREDCON ref=\"TRUE\" />" +
925    "\n <PREDVAR id=\"A\" />" +
926    "\n </IMPL>" +
927    "\n <PREDVAR id=\"A\" />" +
928    "\n </EQUI>" +
929    "\n" +
930    "\n <EQUI>" +
931    "\n <IMPL>" +
932    "\n <PREDCON ref=\"FALSE\" />" +
933    "\n <PREDVAR id=\"A\" />" +
934    "\n </IMPL>" +
935    "\n <PREDCON ref=\"TRUE\" />" +
936    "\n </EQUI>" +
937    "\n" +
938    "\n <EQUI>" +
939    "\n <IMPL>" +
940    "\n <PREDVAR id=\"A\" />" +
941    "\n <PREDCON ref=\"FALSE\" />" +
942    "\n </IMPL>" +
943    "\n <NOT>" +
944    "\n <PREDVAR id=\"A\" />" +
945    "\n </NOT>" +
946    "\n </EQUI>" +
947    "\n" +
948    "\n <EQUI>" +
949    "\n <IMPL>" +
950    "\n <PREDVAR id=\"A\" />" +
951    "\n <PREDCON ref=\"TRUE\" />" +
952    "\n </IMPL>" +
953    "\n <PREDCON ref=\"TRUE\" />" +
954    "\n </EQUI>" +
955    "\n" +
956    "\n <EQUI>" +
957    "\n <EQUI>" +
958    "\n <PREDVAR id=\"A\" />" +
959    "\n <PREDCON ref=\"TRUE\" />" +
960    "\n </EQUI>" +
961    "\n <PREDVAR id=\"A\" />" +
962    "\n </EQUI>" +
963    "\n " +
964    "\n <IMPL>" +
965    "\n <AND>" +
966    "\n <IMPL>" +
967    "\n <PREDVAR id=\"A\" />" +
968    "\n <PREDVAR id=\"B\" />" +
969    "\n </IMPL>" +
970    "\n <IMPL>" +
971    "\n <PREDVAR id=\"B\" />" +
972    "\n <PREDVAR id=\"C\" />" +
973    "\n </IMPL>" +
974    "\n </AND>" +
975    "\n <IMPL>" +
976    "\n <PREDVAR id=\"A\" />" +
977    "\n <PREDVAR id=\"C\" />" +
978    "\n </IMPL>" +
979    "\n </IMPL>" +
980    "\n" +
981    "\n <IMPL>" +
982    "\n <AND>" +
983    "\n <EQUI>" +
984    "\n <PREDVAR id=\"A\" />" +
985    "\n <PREDVAR id=\"B\" />" +
986    "\n </EQUI>" +
987    "\n <EQUI>" +
988    "\n <PREDVAR id=\"C\" />" +
989    "\n <PREDVAR id=\"B\" />" +
990    "\n </EQUI>" +
991    "\n </AND>" +
992    "\n <EQUI>" +
993    "\n <PREDVAR id=\"A\" />" +
994    "\n <PREDVAR id=\"C\" />" +
995    "\n </EQUI>" +
996    "\n </IMPL>" +
997    "\n" +
998    "\n <EQUI>" +
999    "\n <EQUI>" +
1000    "\n <AND>" +
1001    "\n <PREDVAR id=\"A\" />" +
1002    "\n <PREDVAR id=\"B\" />" +
1003    "\n </AND>" +
1004    "\n <AND>" +
1005    "\n <PREDVAR id=\"A\" />" +
1006    "\n <PREDVAR id=\"C\" />" +
1007    "\n </AND>" +
1008    "\n </EQUI>" +
1009    "\n <IMPL>" +
1010    "\n <PREDVAR id=\"A\" />" +
1011    "\n <EQUI>" +
1012    "\n <PREDVAR id=\"B\" />" +
1013    "\n <PREDVAR id=\"C\" />" +
1014    "\n </EQUI>" +
1015    "\n </IMPL>" +
1016    "\n </EQUI>" +
1017    "\n" +
1018    "\n <EQUI>" +
1019    "\n <EQUI>" +
1020    "\n <AND>" +
1021    "\n <PREDVAR id=\"A\" />" +
1022    "\n <PREDVAR id=\"B\" />" +
1023    "\n </AND>" +
1024    "\n <AND>" +
1025    "\n <PREDVAR id=\"A\" />" +
1026    "\n <NOT>" +
1027    "\n <PREDVAR id=\"B\" />" +
1028    "\n </NOT>" +
1029    "\n </AND>" +
1030    "\n </EQUI>" +
1031    "\n <NOT>" +
1032    "\n <PREDVAR id=\"A\" />" +
1033    "\n </NOT>" +
1034    "\n </EQUI>" +
1035    "\n" +
1036    "\n <EQUI>" +
1037    "\n <EQUI>" +
1038    "\n <PREDVAR id=\"A\" />" +
1039    "\n <AND>" +
1040    "\n <PREDVAR id=\"A\" />" +
1041    "\n <PREDVAR id=\"B\" />" +
1042    "\n </AND>" +
1043    "\n </EQUI>" +
1044    "\n <IMPL>" +
1045    "\n <PREDVAR id=\"A\" />" +
1046    "\n <PREDVAR id=\"B\" />" +
1047    "\n </IMPL>" +
1048    "\n </EQUI>" +
1049    "\n" +
1050    "\n <IMPL>" +
1051    "\n <IMPL>" +
1052    "\n <PREDVAR id=\"A\" />" +
1053    "\n <PREDVAR id=\"B\" />" +
1054    "\n </IMPL>" +
1055    "\n <IMPL>" +
1056    "\n <AND>" +
1057    "\n <PREDVAR id=\"A\" />" +
1058    "\n <PREDVAR id=\"C\" />" +
1059    "\n </AND>" +
1060    "\n <AND>" +
1061    "\n <PREDVAR id=\"B\" />" +
1062    "\n <PREDVAR id=\"C\" />" +
1063    "\n </AND>" +
1064    "\n </IMPL>" +
1065    "\n </IMPL>" +
1066    "\n" +
1067    "\n <IMPL>" +
1068    "\n <EQUI>" +
1069    "\n <PREDVAR id=\"A\" />" +
1070    "\n <PREDVAR id=\"B\" />" +
1071    "\n </EQUI>" +
1072    "\n <EQUI>" +
1073    "\n <AND>" +
1074    "\n <PREDVAR id=\"A\" />" +
1075    "\n <PREDVAR id=\"C\" />" +
1076    "\n </AND>" +
1077    "\n <AND>" +
1078    "\n <PREDVAR id=\"B\" />" +
1079    "\n <PREDVAR id=\"C\" />" +
1080    "\n </AND>" +
1081    "\n </EQUI>" +
1082    "\n </IMPL>" +
1083    "\n" +
1084    "\n </AND>" +
1085    "\n");
1086    // System.out.println(ele.toString());
1087  4 assertTrue(isTautology(ele));
1088    }
1089   
1090    /**
1091    * Function: isTautology(Element)
1092    * Type: positive
1093    * Data: f(y) = f(y)
1094    *
1095    * @throws Exception Test failed.
1096    */
 
1097  4 toggle public void testTautology40() throws Exception {
1098  4 final Element ele = BasicParser.createElement(
1099    " <AND>"
1100    + "\n "
1101    + "\n <IMPL>"
1102    + "\n <FORALL>"
1103    + "\n <VAR id=\"x\" />"
1104    + "\n <IMPL>"
1105    + "\n <PREDVAR id=\"\\phi\">"
1106    + "\n <VAR id=\"x\" />"
1107    + "\n </PREDVAR>"
1108    + "\n <PREDVAR id=\"\\psi\">"
1109    + "\n <VAR id=\"x\" />"
1110    + "\n </PREDVAR>"
1111    + "\n </IMPL>"
1112    + "\n </FORALL>"
1113    + "\n <IMPL>"
1114    + "\n <FORALL>"
1115    + "\n <VAR id=\"x\" />"
1116    + "\n <PREDVAR id=\"\\phi\">"
1117    + "\n <VAR id=\"x\" />"
1118    + "\n </PREDVAR>"
1119    + "\n </FORALL>"
1120    + "\n <FORALL>"
1121    + "\n <VAR id=\"x\" />"
1122    + "\n <PREDVAR id=\"\\psi\">"
1123    + "\n <VAR id=\"x\" />"
1124    + "\n </PREDVAR>"
1125    + "\n </FORALL>"
1126    + "\n </IMPL>"
1127    + "\n </IMPL>"
1128    + "\n"
1129    + "\n <IMPL>"
1130    + "\n <FORALL>"
1131    + "\n <VAR id=\"x\" />"
1132    + "\n <IMPL>"
1133    + "\n <PREDVAR id=\"\\phi\">"
1134    + "\n <VAR id=\"x\" />"
1135    + "\n </PREDVAR>"
1136    + "\n <PREDVAR id=\"\\psi\">"
1137    + "\n <VAR id=\"x\" />"
1138    + "\n </PREDVAR>"
1139    + "\n </IMPL>"
1140    + "\n </FORALL>"
1141    + "\n <IMPL>"
1142    + "\n <EXISTS>"
1143    + "\n <VAR id=\"x\" />"
1144    + "\n <PREDVAR id=\"\\phi\">"
1145    + "\n <VAR id=\"x\" />"
1146    + "\n </PREDVAR>"
1147    + "\n </EXISTS>"
1148    + "\n <EXISTS>"
1149    + "\n <VAR id=\"x\" />"
1150    + "\n <PREDVAR id=\"\\psi\">"
1151    + "\n <VAR id=\"x\" />"
1152    + "\n </PREDVAR>"
1153    + "\n </EXISTS>"
1154    + "\n </IMPL>"
1155    + "\n </IMPL>"
1156    + "\n"
1157    + "\n <IMPL>"
1158    + "\n <EXISTS>"
1159    + "\n <VAR id=\"x\" />"
1160    + "\n <AND>"
1161    + "\n <PREDVAR id=\"\\phi\">"
1162    + "\n <VAR id=\"x\" />"
1163    + "\n </PREDVAR>"
1164    + "\n <PREDVAR id=\"\\psi\">"
1165    + "\n <VAR id=\"x\" />"
1166    + "\n </PREDVAR>"
1167    + "\n </AND>"
1168    + "\n </EXISTS>"
1169    + "\n <AND>"
1170    + "\n <EXISTS>"
1171    + "\n <VAR id=\"x\" />"
1172    + "\n <PREDVAR id=\"\\phi\">"
1173    + "\n <VAR id=\"x\" />"
1174    + "\n </PREDVAR>"
1175    + "\n </EXISTS>"
1176    + "\n <EXISTS>"
1177    + "\n <VAR id=\"x\" />"
1178    + "\n <PREDVAR id=\"\\psi\">"
1179    + "\n <VAR id=\"x\" />"
1180    + "\n </PREDVAR>"
1181    + "\n </EXISTS>"
1182    + "\n </AND>"
1183    + "\n </IMPL>"
1184    + "\n"
1185    + "\n <IMPL>"
1186    + "\n <OR>"
1187    + "\n <FORALL>"
1188    + "\n <VAR id=\"x\" />"
1189    + "\n <PREDVAR id=\"\\psi\">"
1190    + "\n <VAR id=\"x\" />"
1191    + "\n </PREDVAR>"
1192    + "\n </FORALL>"
1193    + "\n <FORALL>"
1194    + "\n <VAR id=\"x\" />"
1195    + "\n <PREDVAR id=\"\\psi\">"
1196    + "\n <VAR id=\"x\" />"
1197    + "\n </PREDVAR>"
1198    + "\n </FORALL>"
1199    + "\n </OR>"
1200    + "\n <FORALL>"
1201    + "\n <VAR id=\"x\" />"
1202    + "\n <OR>"
1203    + "\n <PREDVAR id=\"\\phi\">"
1204    + "\n <VAR id=\"x\" />"
1205    + "\n </PREDVAR>"
1206    + "\n <PREDVAR id=\"\\psi\">"
1207    + "\n <VAR id=\"x\" />"
1208    + "\n </PREDVAR>"
1209    + "\n </OR>"
1210    + "\n </FORALL>"
1211    + "\n </IMPL>"
1212    + "\n"
1213    + "\n <EQUI>"
1214    + "\n <EXISTS>"
1215    + "\n <VAR id=\"x\" />"
1216    + "\n <OR>"
1217    + "\n <PREDVAR id=\"\\phi\">"
1218    + "\n <VAR id=\"x\" />"
1219    + "\n </PREDVAR>"
1220    + "\n <PREDVAR id=\"\\psi\">"
1221    + "\n <VAR id=\"x\" />"
1222    + "\n </PREDVAR>"
1223    + "\n </OR>"
1224    + "\n </EXISTS>"
1225    + "\n <OR>"
1226    + "\n <EXISTS>"
1227    + "\n <VAR id=\"x\" />"
1228    + "\n <PREDVAR id=\"\\phi\">"
1229    + "\n <VAR id=\"x\" />"
1230    + "\n </PREDVAR>"
1231    + "\n </EXISTS>"
1232    + "\n <EXISTS>"
1233    + "\n <VAR id=\"x\" />"
1234    + "\n <PREDVAR id=\"\\psi\">"
1235    + "\n <VAR id=\"x\" />"
1236    + "\n </PREDVAR>"
1237    + "\n </EXISTS>"
1238    + "\n </OR>"
1239    + "\n </EQUI>"
1240    + "\n"
1241    + "\n <EQUI>"
1242    + "\n <FORALL>"
1243    + "\n <VAR id=\"x\" />"
1244    + "\n <AND>"
1245    + "\n <PREDVAR id=\"\\phi\">"
1246    + "\n <VAR id=\"x\" />"
1247    + "\n </PREDVAR>"
1248    + "\n <PREDVAR id=\"\\psi\">"
1249    + "\n <VAR id=\"x\" />"
1250    + "\n </PREDVAR>"
1251    + "\n </AND>"
1252    + "\n </FORALL>"
1253    + "\n <AND>"
1254    + "\n <FORALL>"
1255    + "\n <VAR id=\"x\" />"
1256    + "\n <PREDVAR id=\"\\phi\">"
1257    + "\n <VAR id=\"x\" />"
1258    + "\n </PREDVAR>"
1259    + "\n </FORALL>"
1260    + "\n <FORALL>"
1261    + "\n <VAR id=\"x\" />"
1262    + "\n <PREDVAR id=\"\\psi\">"
1263    + "\n <VAR id=\"x\" />"
1264    + "\n </PREDVAR>"
1265    + "\n </FORALL>"
1266    + "\n </AND>"
1267    + "\n </EQUI>"
1268    + "\n"
1269    + "\n <EQUI>"
1270    + "\n <FORALL>"
1271    + "\n <VAR id=\"x\" />"
1272    + "\n <FORALL>"
1273    + "\n <VAR id=\"y\" />"
1274    + "\n <PREDVAR id=\"\\phi\">"
1275    + "\n <VAR id=\"x\" />"
1276    + "\n <VAR id=\"y\" />"
1277    + "\n </PREDVAR>"
1278    + "\n </FORALL>"
1279    + "\n </FORALL>"
1280    + "\n <FORALL>"
1281    + "\n <VAR id=\"y\" />"
1282    + "\n <FORALL>"
1283    + "\n <VAR id=\"x\" />"
1284    + "\n <PREDVAR id=\"\\phi\">"
1285    + "\n <VAR id=\"x\" />"
1286    + "\n <VAR id=\"y\" />"
1287    + "\n </PREDVAR>"
1288    + "\n </FORALL>"
1289    + "\n </FORALL>"
1290    + "\n </EQUI>"
1291    + "\n"
1292    + "\n <EQUI>"
1293    + "\n <EXISTS>"
1294    + "\n <VAR id=\"x\" />"
1295    + "\n <EXISTS>"
1296    + "\n <VAR id=\"y\" />"
1297    + "\n <PREDVAR id=\"\\phi\">"
1298    + "\n <VAR id=\"x\" />"
1299    + "\n <VAR id=\"y\" />"
1300    + "\n </PREDVAR>"
1301    + "\n </EXISTS>"
1302    + "\n </EXISTS>"
1303    + "\n <EXISTS>"
1304    + "\n <VAR id=\"y\" />"
1305    + "\n <EXISTS>"
1306    + "\n <VAR id=\"x\" />"
1307    + "\n <PREDVAR id=\"\\phi\">"
1308    + "\n <VAR id=\"x\" />"
1309    + "\n <VAR id=\"y\" />"
1310    + "\n </PREDVAR>"
1311    + "\n </EXISTS>"
1312    + "\n </EXISTS>"
1313    + "\n </EQUI>"
1314    + "\n"
1315    + "\n <IMPL>"
1316    + "\n <FORALL>"
1317    + "\n <VAR id=\"x\" />"
1318    + "\n <IMPL>"
1319    + "\n <PREDVAR id=\"\\phi\">"
1320    + "\n <VAR id=\"x\" />"
1321    + "\n </PREDVAR>"
1322    + "\n <PREDVAR id=\"A\" />"
1323    + "\n </IMPL>"
1324    + "\n </FORALL>"
1325    + "\n <IMPL>"
1326    + "\n <FORALL>"
1327    + "\n <VAR id=\"x\" />"
1328    + "\n <PREDVAR id=\"\\phi\">"
1329    + "\n <VAR id=\"x\" />"
1330    + "\n </PREDVAR>"
1331    + "\n </FORALL>"
1332    + "\n <PREDVAR id=\"A\" />"
1333    + "\n </IMPL>"
1334    + "\n </IMPL>"
1335    + "\n"
1336    + "\n <EQUI>"
1337    + "\n <FORALL>"
1338    + "\n <VAR id=\"x\" />"
1339    + "\n <IMPL>"
1340    + "\n <PREDVAR id=\"A\" />"
1341    + "\n <PREDVAR id=\"\\phi\">"
1342    + "\n <VAR id=\"x\" />"
1343    + "\n </PREDVAR>"
1344    + "\n </IMPL>"
1345    + "\n </FORALL>"
1346    + "\n <IMPL>"
1347    + "\n <PREDVAR id=\"A\" />"
1348    + "\n <FORALL>"
1349    + "\n <VAR id=\"x\" />"
1350    + "\n <PREDVAR id=\"\\phi\">"
1351    + "\n <VAR id=\"x\" />"
1352    + "\n </PREDVAR>"
1353    + "\n </FORALL>"
1354    + "\n </IMPL>"
1355    + "\n </EQUI>"
1356    + "\n"
1357    + "\n <EQUI>"
1358    + "\n <FORALL>"
1359    + "\n <VAR id=\"x\" />"
1360    + "\n <AND>"
1361    + "\n <PREDVAR id=\"\\phi\">"
1362    + "\n <VAR id=\"x\" />"
1363    + "\n </PREDVAR>"
1364    + "\n <PREDVAR id=\"A\" />"
1365    + "\n </AND>"
1366    + "\n </FORALL>"
1367    + "\n <AND>"
1368    + "\n <FORALL>"
1369    + "\n <VAR id=\"x\" />"
1370    + "\n <PREDVAR id=\"\\phi\">"
1371    + "\n <VAR id=\"x\" />"
1372    + "\n </PREDVAR>"
1373    + "\n </FORALL>"
1374    + "\n <PREDVAR id=\"A\" />"
1375    + "\n </AND>"
1376    + "\n </EQUI>"
1377    + "\n"
1378    + "\n <EQUI>"
1379    + "\n <FORALL>"
1380    + "\n <VAR id=\"x\" />"
1381    + "\n <OR>"
1382    + "\n <PREDVAR id=\"\\phi\">"
1383    + "\n <VAR id=\"x\" />"
1384    + "\n </PREDVAR>"
1385    + "\n <PREDVAR id=\"A\" />"
1386    + "\n </OR>"
1387    + "\n </FORALL>"
1388    + "\n <OR>"
1389    + "\n <FORALL>"
1390    + "\n <VAR id=\"x\" />"
1391    + "\n <PREDVAR id=\"\\phi\">"
1392    + "\n <VAR id=\"x\" />"
1393    + "\n </PREDVAR>"
1394    + "\n </FORALL>"
1395    + "\n <PREDVAR id=\"A\" />"
1396    + "\n </OR>"
1397    + "\n </EQUI>"
1398    + "\n"
1399    + "\n <IMPL>"
1400    + "\n <FORALL>"
1401    + "\n <VAR id=\"x\" />"
1402    + "\n <EQUI>"
1403    + "\n <PREDVAR id=\"\\phi\">"
1404    + "\n <VAR id=\"x\" />"
1405    + "\n </PREDVAR>"
1406    + "\n <PREDVAR id=\"A\" />"
1407    + "\n </EQUI>"
1408    + "\n </FORALL>"
1409    + "\n <EQUI>"
1410    + "\n <FORALL>"
1411    + "\n <VAR id=\"x\" />"
1412    + "\n <PREDVAR id=\"\\phi\">"
1413    + "\n <VAR id=\"x\" />"
1414    + "\n </PREDVAR>"
1415    + "\n </FORALL>"
1416    + "\n <PREDVAR id=\"A\" />"
1417    + "\n </EQUI>"
1418    + "\n </IMPL>"
1419    + "\n"
1420    + "\n <IMPL>"
1421    + "\n <FORALL>"
1422    + "\n <VAR id=\"x\" />"
1423    + "\n <EQUI>"
1424    + "\n <PREDVAR id=\"\\phi\">"
1425    + "\n <VAR id=\"x\" />"
1426    + "\n </PREDVAR>"
1427    + "\n <PREDVAR id=\"\\psi\">"
1428    + "\n <VAR id=\"x\" />"
1429    + "\n </PREDVAR>"
1430    + "\n </EQUI>"
1431    + "\n </FORALL>"
1432    + "\n <EQUI>"
1433    + "\n <FORALL>"
1434    + "\n <VAR id=\"x\" />"
1435    + "\n <PREDVAR id=\"\\phi\">"
1436    + "\n <VAR id=\"x\" />"
1437    + "\n </PREDVAR>"
1438    + "\n </FORALL>"
1439    + "\n <FORALL>"
1440    + "\n <VAR id=\"x\" />"
1441    + "\n <PREDVAR id=\"\\psi\">"
1442    + "\n <VAR id=\"x\" />"
1443    + "\n </PREDVAR>"
1444    + "\n </FORALL>"
1445    + "\n </EQUI>"
1446    + "\n </IMPL>"
1447    + "\n"
1448    + "\n </AND>"
1449    + "\n"
1450    );
1451    // System.out.println(ele.toString());
1452  4 assertTrue(isTautology(ele));
1453    }
1454   
1455    /**
1456    * Function: isTautology(Element)
1457    * Type: negative
1458    * Data: \forall x (\phi(x) <-> A) <-> (\forall x (\phi(x)) <-> A)
1459    * \forall x ( 2 | x) <-> F) <-> (\forall x (2 | x)) <-> F)
1460    * f t
1461    *
1462    * @throws Exception Test failed.
1463    */
 
1464  2 toggle public void testTautology41() throws Exception {
1465  2 final Element ele = BasicParser.createElement(
1466    "\n <EQUI>"
1467    + "\n <FORALL>"
1468    + "\n <VAR id=\"x\" />"
1469    + "\n <EQUI>"
1470    + "\n <PREDVAR id=\"\\phi\">"
1471    + "\n <VAR id=\"x\" />"
1472    + "\n </PREDVAR>"
1473    + "\n <PREDVAR id=\"A\" />"
1474    + "\n </EQUI>"
1475    + "\n </FORALL>"
1476    + "\n <EQUI>"
1477    + "\n <FORALL>"
1478    + "\n <VAR id=\"x\" />"
1479    + "\n <PREDVAR id=\"\\phi\">"
1480    + "\n <VAR id=\"x\" />"
1481    + "\n </PREDVAR>"
1482    + "\n </FORALL>"
1483    + "\n <PREDVAR id=\"A\" />"
1484    + "\n </EQUI>"
1485    + "\n </EQUI>"
1486    );
1487    // System.out.println(ele.toString());
1488  2 assertFalse(isTautology(ele));
1489    }
1490   
1491    /**
1492    * Function: isTautology(Element)
1493    * Type: positive
1494    * Data: \forall x (\phi(x) -> A) -> (\forall x (\phi(x)) -> A)
1495    *
1496    * @throws Exception Test failed.
1497    */
 
1498  4 toggle public void testTautology42() throws Exception {
1499  4 final Element ele = BasicParser.createElement(
1500    "\n <IMPL>"
1501    + "\n <FORALL>"
1502    + "\n <VAR id=\"x\" />"
1503    + "\n <IMPL>"
1504    + "\n <PREDVAR id=\"\\phi\">"
1505    + "\n <VAR id=\"x\" />"
1506    + "\n </PREDVAR>"
1507    + "\n <PREDVAR id=\"A\" />"
1508    + "\n </IMPL>"
1509    + "\n </FORALL>"
1510    + "\n <IMPL>"
1511    + "\n <FORALL>"
1512    + "\n <VAR id=\"x\" />"
1513    + "\n <PREDVAR id=\"\\phi\">"
1514    + "\n <VAR id=\"x\" />"
1515    + "\n </PREDVAR>"
1516    + "\n </FORALL>"
1517    + "\n <PREDVAR id=\"A\" />"
1518    + "\n </IMPL>"
1519    + "\n </IMPL>"
1520   
1521    );
1522    // System.out.println(ele.toString());
1523  4 assertTrue(isTautology(ele));
1524    }
1525   
1526   
1527    /**
1528    * Function: isTautology(Element)
1529    * Type: positive
1530    * Data: \forall z (z \in x <-> z \in y) -> x = y)
1531    *
1532    * @throws Exception Test failed.
1533    */
 
1534  4 toggle public void testTautology43() throws Exception {
1535  4 final Element ele = BasicParser.createElement(
1536    " <IMPL>\n"
1537    + " <FORALL>\n"
1538    + " <VAR id=\"z\"/>\n"
1539    + " <EQUI>\n"
1540    + " <PREDCON ref=\"in\">\n"
1541    + " <VAR id=\"z\"/>\n"
1542    + " <VAR id=\"x\"/>\n"
1543    + " </PREDCON>\n"
1544    + " <PREDCON ref=\"in\">\n"
1545    + " <VAR id=\"z\"/>\n"
1546    + " <VAR id=\"y\"/>\n"
1547    + " </PREDCON>\n"
1548    + " </EQUI>\n"
1549    + " </FORALL>\n"
1550    + " <PREDCON ref=\"l.equal\">\n"
1551    + " <VAR id=\"x\"/>\n"
1552    + " <VAR id=\"y\"/>\n"
1553    + " </PREDCON>\n"
1554    + " </IMPL>\n"
1555    );
1556    // System.out.println(ele.toString());
1557  4 assertTrue(isTautology(ele));
1558    }
1559   
1560   
1561    /**
1562    * Function: isTautology(Element)
1563    * Type: positive
1564    * Data: (y \in {x | \phi(x)} <-> (isSet(y) n \phi(y))
1565    *
1566    * @throws Exception Test failed.
1567    */
 
1568  5 toggle public void testTautology44() throws Exception {
1569  5 final Element ele = BasicParser.createElement(
1570    " <EQUI>\n"
1571    + " <PREDCON ref=\"in\">\n"
1572    + " <VAR id=\"y\"/>\n"
1573    + " <CLASS>\n"
1574    + " <VAR id=\"x\"/>\n"
1575    + " <PREDVAR id=\"\\phi\">\n"
1576    + " <VAR id=\"x\"/>\n"
1577    + " </PREDVAR>\n"
1578    + " </CLASS>\n"
1579    + " </PREDCON>\n"
1580    + " <AND>\n"
1581    + " <PREDCON ref=\"isSet\">\n"
1582    + " <VAR id=\"y\"/>\n"
1583    + " </PREDCON>\n"
1584    + " <PREDVAR id=\"\\phi\">\n"
1585    + " <VAR id=\"y\"/>\n"
1586    + " </PREDVAR>\n"
1587    + " </AND>\n"
1588    + " </EQUI>\n"
1589    );
1590    // System.out.println(ele.toString());
1591  5 Test failure here assertTrue(isTautology(ele));
1592    }
1593   
1594    /**
1595    * Function: isTautology(Element)
1596    * Type: positive
1597    * Data: C(x) = (z | z \nin x}
1598    *
1599    * @throws Exception Test failed.
1600    */
 
1601  2 toggle public void testTautology45() throws Exception {
1602  2 final Element ele = BasicParser.createElement(
1603    "<PREDCON id=\"equal\">\n"
1604    + " <FUNCON id=\"complement\">\n"
1605    + " <VAR id=\"x\" />\n"
1606    + " </FUNCON>\n"
1607    + " <CLASS>\n"
1608    + " <VAR id=\"z\" />\n"
1609    + " <PREDCON ref=\"notIn\">\n"
1610    + " <VAR id=\"z\" />\n"
1611    + " <VAR id=\"x\" />\n"
1612    + " </PREDCON>\n"
1613    + " </CLASS>\n"
1614    + "</PREDCON>\n"
1615    );
1616    // System.out.println(ele.toString());
1617  2 assertTrue(isTautology(ele));
1618    }
1619   
1620    /**
1621    * Function: isTautology(Element)
1622    * Type: positive
1623    * Data: x <= y <-> x n C(y) = 0
1624    *
1625    * @throws Exception Test failed.
1626    */
 
1627  1 toggle public void testTautology46() throws Exception {
1628  1 final Element ele = BasicParser.createElement(
1629    " <EQUI>\n"
1630    + " <PREDCON ref=\"subclass\">\n"
1631    + " <VAR id=\"x\" />\n"
1632    + " <VAR id=\"y\" />\n"
1633    + " </PREDCON>\n"
1634    + " <PREDCON ref=\"l.equal\">\n"
1635    + " <FUNCON ref=\"intersection\">\n"
1636    + " <VAR id=\"x\" />\n"
1637    + " <FUNCON ref=\"complement\">\n"
1638    + " <VAR id=\"y\" />\n"
1639    + " </FUNCON>\n"
1640    + " </FUNCON>\n"
1641    + " <FUNCON ref=\"emptySet\" />\n"
1642    + " </PREDCON>\n"
1643    + " </EQUI>\n"
1644    );
1645    // System.out.println(ele.toString());
1646  1 assertTrue(isTautology(ele));
1647    }
1648   
1649    /**
1650    * Function: isTautology(Element)
1651    * Type: positive
1652    * Data: see below
1653    *
1654    * @throws Exception Test failed.
1655    */
 
1656  1 toggle public void testTautology47() throws Exception {
1657  1 final Element ele = BasicParser.createElement(
1658    "<AND>\n"
1659    + " <EQUI>\n"
1660    + " <PREDCON ref=\"subclass\">\n"
1661    + " <VAR id=\"x\" />\n"
1662    + " <VAR id=\"y\" />\n"
1663    + " </PREDCON>\n"
1664    + " <PREDCON ref=\"l.equal\">\n"
1665    + " <FUNCON ref=\"union\">\n"
1666    + " <FUNCON ref=\"complement\">\n"
1667    + " <VAR id=\"x\" />\n"
1668    + " </FUNCON>\n"
1669    + " <VAR id=\"y\" />\n"
1670    + " </FUNCON>\n"
1671    + " <FUNCON ref=\"universalClass\" />\n"
1672    + " </PREDCON>\n"
1673    + " </EQUI>\n"
1674    + " \n"
1675    + " <EQUI>\n"
1676    + " <PREDCON ref=\"subclass\">\n"
1677    + " <VAR id=\"x\" />\n"
1678    + " <FUNCON ref=\"complement\">\n"
1679    + " <VAR id=\"y\" />\n"
1680    + " </FUNCON>\n"
1681    + " </PREDCON>\n"
1682    + " <PREDCON ref=\"l.equal\">\n"
1683    + " <FUNCON ref=\"intersection\">\n"
1684    + " <VAR id=\"x\" />\n"
1685    + " <VAR id=\"y\" />\n"
1686    + " </FUNCON>\n"
1687    + " <FUNCON ref=\"emptySet\" />\n"
1688    + " </PREDCON>\n"
1689    + " </EQUI>\n"
1690    + " \n"
1691    + " <EQUI>\n"
1692    + " <PREDCON ref=\"subclass\">\n"
1693    + " <FUNCON ref=\"intersection\">\n"
1694    + " <VAR id=\"x\" />\n"
1695    + " <VAR id=\"y\" />\n"
1696    + " </FUNCON>\n"
1697    + " <VAR id=\"z\" />\n"
1698    + " </PREDCON>\n"
1699    + " <PREDCON ref=\"subclass\">\n"
1700    + " <VAR id=\"x\" />\n"
1701    + " <FUNCON ref=\"union\">\n"
1702    + " <FUNCON ref=\"complement\">\n"
1703    + " <VAR id=\"y\" />\n"
1704    + " </FUNCON>\n"
1705    + " <VAR id=\"z\" />\n"
1706    + " </FUNCON>\n"
1707    + " </PREDCON>\n"
1708    + " </EQUI> \n"
1709    + " \n"
1710    + "</AND>\n"
1711    );
1712    // System.out.println(ele.toString());
1713  1 assertTrue(isTautology(ele));
1714    }
1715   
1716    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .