01 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
02 *
03 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
04 *
05 * "Hilbert II" is free software; you can redistribute
06 * it and/or modify it under the terms of the GNU General Public
07 * License as published by the Free Software Foundation; either
08 * version 2 of the License, or (at your option) any later version.
09 *
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.work;
17
18 import org.qedeq.kernel.bo.logic.common.LogicalCheckException;
19 import org.qedeq.kernel.bo.logic.common.Operators;
20 import org.qedeq.kernel.bo.logic.wf.FormulaCheckException;
21 import org.qedeq.kernel.se.base.list.Element;
22
23
24 /**
25 * This class deals with {@link org.qedeq.kernel.se.base.list.Element}s and could check
26 * if two formulas are logically equivalent.
27 *
28 * LATER mime 20050205: work in progress
29 *
30 * @author Michael Meyling
31 */
32 public final class LogicalEquivalence {
33
34 /**
35 * Constructor.
36 */
37 private LogicalEquivalence() {
38 // nothing to do
39 }
40
41 /**
42 * Assures that two words are logically equivalent.
43 *
44 * @param formula1 First formula.
45 * @param formula2 Second formula.
46 * @throws LogicalCheckException Check failed.
47 */
48 public static final void checkEquivalence(final Element formula1,
49 final Element formula2)
50 throws LogicalCheckException {
51 if (formula1.equals(formula2)) {
52 return;
53 }
54 if (formula1.isAtom() || formula2.isAtom()) {
55 return; // LATER mime 20050330: where is the check???
56 }
57 final String op1 = formula1.getList().getOperator();
58 final String op2 = formula2.getList().getOperator();
59 if (op1.equals(op2) && (op1.equals(Operators.CONJUNCTION_OPERATOR)
60 || op1.equals(Operators.DISJUNCTION_OPERATOR))) {
61 final EqualFormulaSet sub1 = new EqualFormulaSet(formula1.getList());
62 final EqualFormulaSet sub2 = new EqualFormulaSet(formula2.getList());
63 if (sub1.equals(sub2)) {
64 return;
65 }
66
67 }
68 throw new FormulaCheckException(61, "no logical equivalence found", formula2, null);
69 }
70
71 }
|