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