EMMA Coverage Report (generated Fri Feb 14 08:28:31 UTC 2014)
[all classes][org.qedeq.kernel.bo.logic.proof.checker]

COVERAGE SUMMARY FOR SOURCE FILE [ProofChecker2Impl.java]

nameclass, %method, %block, %line, %
ProofChecker2Impl.java100% (2/2)80%  (28/35)38%  (1260/3301)42%  (231.5/554)

COVERAGE BREAKDOWN BY CLASS AND METHOD

nameclass, %method, %block, %line, %
     
class ProofChecker2Impl100% (1/1)79%  (22/28)37%  (1182/3182)41%  (221.5/538)
check (Existential, int, Element): boolean 0%   (0/1)0%   (0/235)0%   (0/42)
check (SubstFunc, int, Element): boolean 0%   (0/1)0%   (0/337)0%   (0/64)
checkRule (Rule, ModuleContext, RuleChecker, ReferenceResolver): LogicalCheck... 0%   (0/1)0%   (0/48)0%   (0/6)
getDiffModuleContextOfProofLineFormula (int, Element): ModuleContext 0%   (0/1)0%   (0/61)0%   (0/4)
getReferenceContext (String): ModuleContext 0%   (0/1)0%   (0/36)0%   (0/4)
handleProofCheckException (int, String, ModuleContext, ModuleContext): void 0%   (0/1)0%   (0/14)0%   (0/3)
check (ModusPonens, int, Element): boolean 100% (1/1)25%  (69/271)41%  (17/41)
check (Add, int, Element): boolean 100% (1/1)30%  (54/181)38%  (12/32)
check (SubstFree, int, Element): boolean 100% (1/1)30%  (57/188)39%  (12.4/32)
check (Universal, int, Element): boolean 100% (1/1)32%  (76/235)44%  (18.4/42)
addLocalLineLabel (int, String): void 100% (1/1)33%  (27/83)60%  (6/10)
check (Rename, int, Element): boolean 100% (1/1)33%  (55/165)46%  (12.4/27)
check (SubstPred, int, Element): boolean 100% (1/1)34%  (113/337)38%  (24.4/64)
isProvedFormula (String): boolean 100% (1/1)50%  (10/20)67%  (2/3)
getNormalizedReferenceFormula (String): Element 100% (1/1)56%  (10/18)67%  (2/3)
getModuleContextOfProofLineFormula (int): ModuleContext 100% (1/1)56%  (27/48)67%  (2/3)
check (ConditionalProof, int, Element): boolean 100% (1/1)60%  (211/353)52%  (31/60)
checkProof (ElementList, Element, FormalProofLineList, RuleChecker, ModuleCon... 100% (1/1)83%  (358/431)81%  (57/70)
isLocalProofLineReference (String): boolean 100% (1/1)83%  (10/12)67%  (2/3)
getNormalizedProofLine (Integer): Element 100% (1/1)85%  (22/26)67%  (4/6)
ProofChecker2Impl (): void 100% (1/1)100% (16/16)100% (5/5)
checkProof (Element, FormalProofLineList, RuleChecker, ModuleContext, Referen... 100% (1/1)100% (14/14)100% (2/2)
getCurrentContext (): ModuleContext 100% (1/1)100% (3/3)100% (1/1)
getNormalizedFormula (Element): Element 100% (1/1)100% (5/5)100% (1/1)
getNormalizedLocalProofLineReference (String): Element 100% (1/1)100% (20/20)100% (4/4)
handleProofCheckException (int, String, ModuleContext): void 100% (1/1)100% (12/12)100% (3/3)
hasConditions (): boolean 100% (1/1)100% (8/8)100% (1/1)
setLocationWithinModule (String): void 100% (1/1)100% (5/5)100% (2/2)
     
class ProofChecker2Impl$1100% (1/1)86%  (6/7)66%  (78/119)65%  (11/17)
getReferenceContext (String): ModuleContext 0%   (0/1)0%   (0/27)0%   (0/3)
getNormalizedReferenceFormula (String): Element 100% (1/1)55%  (12/22)67%  (2/3)
isLocalProofLineReference (String): boolean 100% (1/1)86%  (12/14)67%  (2/3)
isProvedFormula (String): boolean 100% (1/1)86%  (12/14)67%  (2/3)
ProofChecker2Impl$1 (ProofChecker2Impl, ConditionalProof, ModuleAddress, Stri... 100% (1/1)100% (15/15)100% (1/1)
getNormalizedFormula (Element): Element 100% (1/1)100% (5/5)100% (1/1)
getNormalizedLocalProofLineReference (String): Element 100% (1/1)100% (22/22)100% (3/3)

1/* This file is part of the project "Hilbert II" - http://www.qedeq.org
2 *
3 * Copyright 2000-2014,  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 
16package org.qedeq.kernel.bo.logic.proof.checker;
17 
18import java.util.HashMap;
19import java.util.Map;
20 
21import org.qedeq.base.io.Version;
22import org.qedeq.base.io.VersionSet;
23import org.qedeq.base.utility.Enumerator;
24import org.qedeq.base.utility.EqualsUtility;
25import org.qedeq.base.utility.StringUtility;
26import org.qedeq.kernel.bo.logic.common.FormulaChecker;
27import org.qedeq.kernel.bo.logic.common.FormulaUtility;
28import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
29import org.qedeq.kernel.bo.logic.common.Operators;
30import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
31import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
32import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
33import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
34import org.qedeq.kernel.se.base.list.Element;
35import org.qedeq.kernel.se.base.list.ElementList;
36import org.qedeq.kernel.se.base.module.Add;
37import org.qedeq.kernel.se.base.module.ConditionalProof;
38import org.qedeq.kernel.se.base.module.Existential;
39import org.qedeq.kernel.se.base.module.FormalProofLine;
40import org.qedeq.kernel.se.base.module.FormalProofLineList;
41import org.qedeq.kernel.se.base.module.ModusPonens;
42import org.qedeq.kernel.se.base.module.Reason;
43import org.qedeq.kernel.se.base.module.Rename;
44import org.qedeq.kernel.se.base.module.Rule;
45import org.qedeq.kernel.se.base.module.SubstFree;
46import org.qedeq.kernel.se.base.module.SubstFunc;
47import org.qedeq.kernel.se.base.module.SubstPred;
48import org.qedeq.kernel.se.base.module.Universal;
49import org.qedeq.kernel.se.common.ModuleAddress;
50import org.qedeq.kernel.se.common.ModuleContext;
51import org.qedeq.kernel.se.common.RuleKey;
52import org.qedeq.kernel.se.dto.list.DefaultElementList;
53import org.qedeq.kernel.se.dto.list.ElementSet;
54 
55 
56/**
57 * Formal proof checker for basic rules and conditional proof.
58 *
59 * @author  Michael Meyling
60 */
61public class ProofChecker2Impl implements ProofChecker, ReferenceResolver {
62 
63    /** Proof we want to check. */
64    private FormalProofLineList proof;
65 
66    /** Module context of proof line list. */
67    private ModuleContext moduleContext;
68 
69    /** Current context. */
70    private ModuleContext currentContext;
71 
72    /** Resolver for external references. */
73    private ReferenceResolver resolver;
74 
75    /** All exceptions that occurred during checking. */
76    private LogicalCheckExceptionList exceptions;
77 
78    /** Array with proof status for each proof line. */
79    private boolean[] lineProved;
80 
81    /** Maps local proof line labels to local line number Integers. */
82    private Map label2line;
83 
84    /** Rule version we support. */
85    private final VersionSet supported;
86 
87    /** These preconditions apply. This is a conjunction with 0 to n elements. */
88    private ElementList conditions;
89 
90    /** Rule existence checker. */
91    private RuleChecker checker;
92 
93    /**
94     * Constructor.
95     */
96    public ProofChecker2Impl() {
97        supported = new VersionSet();
98        supported.add("0.01.00");
99        supported.add("0.02.00");
100    }
101 
102    public LogicalCheckExceptionList checkRule(final Rule rule,
103            final ModuleContext context, final RuleChecker checker,
104            final ReferenceResolver resolver) {
105        exceptions = new LogicalCheckExceptionList();
106        final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
107        if (rule.getVersion() == null || !supported.contains(rule.getVersion())) {
108            final ProofCheckException ex = new ProofCheckException(
109                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
110                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + ruleKey
111                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
112                context);
113            exceptions.add(ex);
114        }
115        return exceptions;
116    }
117 
118    public LogicalCheckExceptionList checkProof(final Element formula,
119            final FormalProofLineList proof,
120            final RuleChecker checker,
121            final ModuleContext moduleContext,
122            final ReferenceResolver resolver) {
123        final DefaultElementList con = new DefaultElementList(
124            Operators.CONJUNCTION_OPERATOR);
125        // we have no conditions, so we add an empty condition
126        return checkProof(con, formula, proof, checker, moduleContext, resolver);
127    }
128 
129    private LogicalCheckExceptionList checkProof(final ElementList conditions, final Element formula,
130            final FormalProofLineList proof,
131            final RuleChecker checker,
132            final ModuleContext moduleContext,
133            final ReferenceResolver resolver) {
134        this.conditions = conditions;
135        this.proof = proof;
136        this.checker = checker;
137        this.resolver = resolver;
138        this.moduleContext = moduleContext;
139        // use copy constructor for changing context
140        currentContext = new ModuleContext(moduleContext);
141        exceptions = new LogicalCheckExceptionList();
142        final String context = moduleContext.getLocationWithinModule();
143        lineProved = new boolean[proof.size()];
144        label2line = new HashMap();
145        for (int i = 0; i < proof.size(); i++) {
146            boolean ok = true;
147            setLocationWithinModule(context + ".get(" + i + ")");
148            final FormalProofLine line = proof.get(i);
149            if (line == null || line.getFormula() == null
150                    || line.getFormula().getElement() == null) {
151                ok = false;
152                handleProofCheckException(
153                    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
154                    BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
155                    getCurrentContext());
156                continue;
157            }
158            setLocationWithinModule(context + ".get(" + i + ").getReason()");
159            final Reason reason = line.getReason();
160            if (reason == null) {
161                ok = false;
162                handleProofCheckException(
163                    BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
164                    BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
165                    getCurrentContext());
166                continue;
167            }
168            if (line.getLabel() != null && line.getLabel().length() > 0) {
169                setLocationWithinModule(context + ".get(" + i + ").getLabel()");
170                addLocalLineLabel(i, line.getLabel());
171            }
172 
173            // check if the formula together with the conditions is well formed
174            if (hasConditions()) {
175                setLocationWithinModule(context + ".get(" + i + ").getFormula.getElement()");
176                ElementList full = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
177                if (conditions.size() > 1) {
178                    full.add(conditions);
179                } else {
180                    full.add(conditions.getElement(0));
181                }
182                full.add(line.getFormula().getElement());
183                FormulaChecker checkWf = new FormulaCheckerImpl();  // TODO 20110612 m31: use factory?
184                final LogicalCheckExceptionList list = checkWf.checkFormula(full, getCurrentContext());
185                if (list.size() > 0) {
186                    ok = false;
187                    handleProofCheckException(
188                        BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_CODE,
189                        BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_TEXT
190                        + list.get(0).getMessage(),
191                        getCurrentContext());
192                    continue;
193                }
194            }
195 
196            // check if only defined rules are used
197            // TODO 20110316 m31: this is a dirty trick to get the context of the reason
198            //                    perhaps we can solve this more elegantly?
199            String getReason = ".get" + StringUtility.getClassName(reason.getClass());
200            if (getReason.endsWith("Vo")) {
201                getReason = getReason.substring(0, getReason.length() - 2) + "()";
202                setLocationWithinModule(context + ".get(" + i + ").getReason()"
203                    + getReason);
204//                System.out.println(getCurrentContext());
205            }
206            if (reason instanceof Add) {
207                ok = check((Add) reason, i, line.getFormula().getElement());
208            } else if (reason instanceof Rename) {
209                ok = check((Rename) reason, i, line.getFormula().getElement());
210            } else if (reason instanceof ModusPonens) {
211                ok = check((ModusPonens) reason, i, line.getFormula().getElement());
212            } else if (reason instanceof SubstFree) {
213                ok = check((SubstFree) reason, i, line.getFormula().getElement());
214            } else if (reason instanceof SubstPred) {
215                ok = check((SubstPred) reason, i, line.getFormula().getElement());
216            } else if (reason instanceof SubstFunc) {
217                ok = check((SubstFunc) reason, i, line.getFormula().getElement());
218            } else if (reason instanceof Universal) {
219                ok = check((Universal) reason, i, line.getFormula().getElement());
220            } else if (reason instanceof Existential) {
221                ok = check((Existential) reason, i, line.getFormula().getElement());
222            } else if (reason instanceof ConditionalProof) {
223                setLocationWithinModule(context + ".get(" + i + ")");
224                ok = check((ConditionalProof) reason, i, line.getFormula().getElement());
225            } else {
226                ok = false;
227                handleProofCheckException(
228                    BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
229                    BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
230                    + reason.getName(),
231                    getCurrentContext());
232            }
233            lineProved[i] = ok;
234            // check if last proof line is identical with proposition formula
235            if (i == proof.size() - 1) {
236                if (!formula.equals(line.getFormula().getElement())) {
237                    handleProofCheckException(
238                        BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
239                        BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT,
240                        getModuleContextOfProofLineFormula(i));
241                }
242            }
243        }
244        return exceptions;
245    }
246 
247    private void addLocalLineLabel(final int i, final String label) {
248        if (label != null && label.length() > 0) {
249            final Integer n = (Integer) label2line.get(label);
250            if (n != null) {
251                final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
252                    moduleContext.getLocationWithinModule() + ".get("
253                    + label2line.get(label)
254                    + ").getLabel()");
255                handleProofCheckException(
256                    BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
257                    BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
258                    + label,
259                    getCurrentContext(),
260                    lc);
261            } else {
262                if (isLocalProofLineReference(label)) {
263                    handleProofCheckException(
264                        BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
265                        BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
266                        + label,
267                        getCurrentContext(),
268                        resolver.getReferenceContext(label));
269//                    System.out.println("we hava label already: " + label);
270//                    ProofFinderUtility.println(getNormalizedLocalProofLineReference(label));
271                }
272            }
273//            System.out.println("adding label: " + label);
274            label2line.put(label, new Integer(i));
275        }
276    }
277 
278    private boolean check(final Add add, final int i, final Element element) {
279        final String context = currentContext.getLocationWithinModule();
280        boolean ok = true;
281        if (add.getReference() == null) {
282            ok = false;
283            setLocationWithinModule(context + ".getReference()");
284            handleProofCheckException(
285                BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
286                BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
287                getCurrentContext());
288            return ok;
289        }
290        if (!resolver.isProvedFormula(add.getReference())) {
291            ok = false;
292            setLocationWithinModule(context + ".getReference()");
293            handleProofCheckException(
294                BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
295                BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
296                + add.getReference(),
297                getCurrentContext());
298            return ok;
299        }
300        final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
301        final Element current = resolver.getNormalizedFormula(element);
302        if (!EqualsUtility.equals(expected, current)) {
303            ok = false;
304            handleProofCheckException(
305                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
306                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
307                + add.getReference(),
308                getDiffModuleContextOfProofLineFormula(i, expected));
309            return ok;
310        }
311        final RuleKey defined = checker.getRule(add.getName());
312        if (defined == null) {
313            ok = false;
314            handleProofCheckException(
315                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
316                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
317                + add.getName(),
318                getCurrentContext());
319            return ok;
320        } else if (!supported.contains(defined.getVersion())) {
321            ok = false;
322            handleProofCheckException(
323                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
324                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
325                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
326                getCurrentContext());
327            return ok;
328        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
329            ok = false;
330            handleProofCheckException(
331                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
332                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
333                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
334                getCurrentContext());
335            return ok;
336        }
337        return ok;
338    }
339 
340    private boolean check(final Rename rename, final int i, final Element element) {
341        final String context = currentContext.getLocationWithinModule();
342        boolean ok = true;
343        final Element f = getNormalizedLocalProofLineReference(rename.getReference());
344        if (f == null) {
345            ok = false;
346            setLocationWithinModule(context + ".getReference()");
347            handleProofCheckException(
348                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
349                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
350                + rename.getReference(),
351                getCurrentContext());
352        } else {
353            final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
354                rename.getOriginalSubjectVariable(),
355                rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
356                new Enumerator());
357            final Element current = resolver.getNormalizedFormula(element);
358            if (!EqualsUtility.equals(expected, current)) {
359                ok = false;
360                handleProofCheckException(
361                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
362                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
363                    + rename.getReference(),
364                    getDiffModuleContextOfProofLineFormula(i, expected));
365            } else {
366                ok = true;
367            }
368        }
369        final RuleKey defined = checker.getRule(rename.getName());
370        if (defined == null) {
371            ok = false;
372            handleProofCheckException(
373                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
374                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
375                + rename.getName(),
376                getCurrentContext());
377            return ok;
378        } else if (!supported.contains(defined.getVersion())) {
379            ok = false;
380            handleProofCheckException(
381                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
382                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
383                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
384                getCurrentContext());
385            return ok;
386        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
387            ok = false;
388            handleProofCheckException(
389                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
390                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
391                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
392                getCurrentContext());
393            return ok;
394        }
395        return ok;
396    }
397 
398    private boolean check(final SubstFree substFree, final int i, final Element element) {
399        final String context = currentContext.getLocationWithinModule();
400        boolean ok = true;
401        final Element f = getNormalizedLocalProofLineReference(substFree.getReference());
402        if (f == null) {
403            ok = false;
404            setLocationWithinModule(context + ".getReference()");
405            handleProofCheckException(
406                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
407                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
408                + substFree.getReference(),
409                getCurrentContext());
410        } else {
411            final Element current = resolver.getNormalizedFormula(element);
412            final Element expected = f.replace(substFree.getSubjectVariable(),
413                resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
414            if (!EqualsUtility.equals(current, expected)) {
415                ok = false;
416                handleProofCheckException(
417                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
418                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
419                    + substFree.getReference(),
420                    getDiffModuleContextOfProofLineFormula(i, expected));
421                return ok;
422            }
423        }
424        // check precondition: subject variable doesn't occur in a precondition
425        if (FormulaUtility.containsOperatorVariable(conditions, substFree.getSubjectVariable())) {
426            ok = false;
427            setLocationWithinModule(context + ".getSubstituteFormula()");
428            handleProofCheckException(
429                BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
430                BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
431                getCurrentContext());
432            return ok;
433        }
434        final RuleKey defined = checker.getRule(substFree.getName());
435        if (defined == null) {
436            ok = false;
437            handleProofCheckException(
438                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
439                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
440                + substFree.getName(),
441                getCurrentContext());
442            return ok;
443        } else if (!supported.contains(defined.getVersion())) {
444            ok = false;
445            handleProofCheckException(
446                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
447                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
448                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
449                getCurrentContext());
450            return ok;
451        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
452            ok = false;
453            handleProofCheckException(
454                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
455                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
456                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
457                getCurrentContext());
458            return ok;
459        }
460        return ok;
461    }
462 
463    private boolean check(final SubstPred substPred, final int i, final Element element) {
464        final String context = currentContext.getLocationWithinModule();
465        boolean ok = true;
466        final Element alpha = getNormalizedLocalProofLineReference(substPred.getReference());
467        if (alpha == null) {
468            ok = false;
469            setLocationWithinModule(context + ".getReference()");
470            handleProofCheckException(
471                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
472                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
473                + substPred.getReference(),
474                getCurrentContext());
475            return ok;
476        }
477        final Element current = resolver.getNormalizedFormula(element);
478        if (substPred.getSubstituteFormula() == null) {
479            ok = false;
480            handleProofCheckException(
481                BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
482                BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
483                getCurrentContext());
484            return ok;
485        }
486        final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
487        final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
488        final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
489        if (!EqualsUtility.equals(current, expected)) {
490            ok = false;
491            handleProofCheckException(
492                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
493                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
494                + substPred.getReference(),
495                getDiffModuleContextOfProofLineFormula(i, expected));
496            return ok;
497        }
498        // check precondition: predicate variable p must have n pairwise different free subject
499        // variables as arguments
500        final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
501        if (predFree.size() != p.getList().size() - 1) {
502            ok = false;
503            setLocationWithinModule(context + ".getPredicateVariable()");
504            handleProofCheckException(
505                BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
506                BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
507                getDiffModuleContextOfProofLineFormula(i, expected));
508            return ok;
509        }
510        for (int j = 1; j < p.getList().size(); j++) {
511            if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
512                ok = false;
513                setLocationWithinModule(context + ".getPredicateVariable()");
514                handleProofCheckException(
515                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
516                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
517                    getCurrentContext());
518                return ok;
519            }
520        }
521        // check precondition: the free variables of $\beta(x_1, \ldots, x_n)$ without
522        // $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
523        final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
524        final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
525        if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
526            ok = false;
527            setLocationWithinModule(context + ".getSubstituteFormula()");
528            handleProofCheckException(
529                BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
530                BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
531                getCurrentContext());
532            return ok;
533        }
534        // check precondition: each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains
535        // no bound variable of $\beta(x_1, \ldots, x_n)$
536        final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
537        if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
538            ok = false;
539            setLocationWithinModule(context + ".getSubstituteFormula()");
540            handleProofCheckException(
541                BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
542                BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
543                getCurrentContext());
544            return ok;
545        }
546        // check precondition: $\sigma(...)$ dosn't occur in a precondition
547        if (FormulaUtility.containsOperatorVariable(conditions, p)) {
548            ok = false;
549            setLocationWithinModule(context + ".getPredicateVariable()");
550            handleProofCheckException(
551                BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
552                BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
553                getCurrentContext());
554            return ok;
555        }
556        // check precondition: resulting formula is well formed was already done by well formed
557        // checker
558 
559        final RuleKey defined = checker.getRule(substPred.getName());
560        if (defined == null) {
561            ok = false;
562            handleProofCheckException(
563                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
564                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
565                + substPred.getName(),
566                getCurrentContext());
567            return ok;
568        } else if (!supported.contains(defined.getVersion())) {
569            ok = false;
570            handleProofCheckException(
571                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
572                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
573                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
574                getCurrentContext());
575            return ok;
576        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
577            ok = false;
578            handleProofCheckException(
579                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
580                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
581                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
582                getCurrentContext());
583            return ok;
584        }
585        return ok;
586    }
587 
588    private boolean check(final SubstFunc substFunc, final int i, final Element element) {
589        final String context = currentContext.getLocationWithinModule();
590        boolean ok = true;
591        final Element alpha = getNormalizedLocalProofLineReference(substFunc.getReference());
592        if (alpha == null) {
593            ok = false;
594            setLocationWithinModule(context + ".getReference()");
595            handleProofCheckException(
596                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
597                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
598                + substFunc.getReference(),
599                getCurrentContext());
600            return ok;
601        }
602        final Element current = resolver.getNormalizedFormula(element);
603        if (substFunc.getSubstituteTerm() == null) {
604            ok = false;
605            handleProofCheckException(
606                BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
607                BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
608                getCurrentContext());
609            return ok;
610        }
611        final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
612        final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
613        final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
614        if (!EqualsUtility.equals(current, expected)) {
615            ok = false;
616            handleProofCheckException(
617                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
618                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
619                + substFunc.getReference(),
620                getDiffModuleContextOfProofLineFormula(i, expected));
621            return ok;
622        }
623        // check precondition: function variable $\sigma$ must have n pairwise different free
624        // subject variables as arguments
625        final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
626        if (funcFree.size() != sigma.getList().size() - 1) {
627            ok = false;
628            setLocationWithinModule(context + ".getPredicateVariable()");
629            handleProofCheckException(
630                BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
631                BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
632                getDiffModuleContextOfProofLineFormula(i, expected));
633            return ok;
634        }
635        for (int j = 1; j < sigma.getList().size(); j++) {
636            if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
637                ok = false;
638                setLocationWithinModule(context + ".getPredicateVariable()");
639                handleProofCheckException(
640                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
641                    BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
642                    getCurrentContext());
643                return ok;
644            }
645        }
646        // check precondition: the free variables of $\tau(x_1, \ldots, x_n)$
647        // without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
648        final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
649        final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
650        if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
651            ok = false;
652            setLocationWithinModule(context + ".getSubstituteFormula()");
653            handleProofCheckException(
654                BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
655                BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
656                getCurrentContext());
657            return ok;
658        }
659        // check precondition: each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$
660        // contains no bound variable of $\tau(x_1, \ldots, x_n)$
661        final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
662        if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
663            ok = false;
664            setLocationWithinModule(context + ".getSubstituteFormula()");
665            handleProofCheckException(
666                BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
667                BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
668                getCurrentContext());
669            return ok;
670        }
671        // check precondition: $\sigma(...)$ dosn't occur in a precondition
672        if (FormulaUtility.containsOperatorVariable(conditions, sigma)) {
673            ok = false;
674            setLocationWithinModule(context + ".getPredicateVariable()");
675            handleProofCheckException(
676                BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE,
677                BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT,
678                getCurrentContext());
679            return ok;
680        }
681        // check precondition: resulting formula is well formed was already done by well formed
682        // checker
683 
684        final RuleKey defined = checker.getRule(substFunc.getName());
685        if (defined == null) {
686            ok = false;
687            handleProofCheckException(
688                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
689                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
690                + substFunc.getName(),
691                getCurrentContext());
692            return ok;
693        } else if (!supported.contains(defined.getVersion())) {
694            ok = false;
695            handleProofCheckException(
696                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
697                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
698                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
699                getCurrentContext());
700            return ok;
701        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
702            ok = false;
703            handleProofCheckException(
704                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
705                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
706                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
707                getCurrentContext());
708            return ok;
709        }
710        return ok;
711    }
712 
713    private boolean check(final ModusPonens mp, final int i, final Element element) {
714        final String context = currentContext.getLocationWithinModule();
715        boolean ok = true;
716        final Element f1 = getNormalizedLocalProofLineReference(mp.getReference1());
717        if (f1 == null) {
718            ok = false;
719            setLocationWithinModule(context + ".getReference1()");
720            handleProofCheckException(
721                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
722                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
723                + mp.getReference1(),
724                getCurrentContext());
725        }
726        final Element f2 = getNormalizedLocalProofLineReference(mp.getReference2());
727        if (f2 == null) {
728            ok = false;
729            setLocationWithinModule(context + ".getReference2()");
730            handleProofCheckException(
731                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
732                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
733                + mp.getReference2(),
734                getCurrentContext());
735        }
736        if (ok) {
737            final Element current = getNormalizedFormula(element);
738            if (!FormulaUtility.isImplication(f1)) {
739                ok = false;
740                setLocationWithinModule(context + ".getReference1()");
741                handleProofCheckException(
742                    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
743                    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
744                    + mp.getReference1(),
745                    getCurrentContext());
746            } else if (!f2.equals(f1.getList().getElement(0))) {
747                ok = false;
748                setLocationWithinModule(context + ".getReference2()");
749                handleProofCheckException(
750                    BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
751                    BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
752                    + mp.getReference2(),
753                    getCurrentContext(),
754                    resolver.getReferenceContext(mp.getReference1()));
755            } else if (!current.equals(f1.getList().getElement(1))) {
756                ok = false;
757                setLocationWithinModule(context + ".getReference1()");
758                handleProofCheckException(
759                    BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
760                    BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
761                    + mp.getReference1(),
762                    getCurrentContext(),
763                    resolver.getReferenceContext(mp.getReference1()));
764            } else {
765                ok = true;
766            }
767        }
768        final RuleKey defined = checker.getRule(mp.getName());
769        if (defined == null) {
770            ok = false;
771            handleProofCheckException(
772                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
773                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
774                + mp.getName(),
775                getCurrentContext());
776            return ok;
777        } else if (!supported.contains(defined.getVersion())) {
778            ok = false;
779            handleProofCheckException(
780                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
781                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
782                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
783                getCurrentContext());
784            return ok;
785        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
786            ok = false;
787            handleProofCheckException(
788                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
789                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
790                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
791                getCurrentContext());
792            return ok;
793        }
794        return ok;
795    }
796 
797    private boolean check(final Universal universal, final int i, final Element element) {
798        final String context = currentContext.getLocationWithinModule();
799        boolean ok = true;
800        final Element reference = getNormalizedLocalProofLineReference(universal.getReference());
801        if (reference == null) {
802            ok = false;
803            setLocationWithinModule(context + ".getReference()");
804            handleProofCheckException(
805                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
806                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
807                + universal.getReference(),
808                getCurrentContext());
809//        } else if (!lineProved[n.intValue()]) {
810//            ok = false;
811//            setLocationWithinModule(context + ".getReference()");
812//            handleProofCheckException(
813//                BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
814//                BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
815//                + universal.getReference(),
816//                getCurrentContext());
817        } else {
818            final Element current = getNormalizedFormula(element);
819            if (!FormulaUtility.isImplication(current)) {
820                ok = false;
821                setLocationWithinModule(context + ".getReference()");
822                handleProofCheckException(
823                    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
824                    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
825                    + universal.getReference(),
826                    getCurrentContext());
827                return ok;
828            }
829            if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
830                ok = false;
831                setLocationWithinModule(context + ".getSubjectVariable()");
832                handleProofCheckException(
833                    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
834                    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
835                    getCurrentContext());
836                return ok;
837            }
838            final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
839            expected.add(reference.getList().getElement(0));
840            final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
841            uni.add(universal.getSubjectVariable());
842            uni.add(reference.getList().getElement(1));
843            expected.add(uni);
844//            System.out.print("Expected: ");
845//            ProofFinderUtility.println(expected);
846//            System.out.print("Current : ");
847//            ProofFinderUtility.println(current);
848            if (!EqualsUtility.equals(current, expected)) {
849                ok = false;
850                handleProofCheckException(
851                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
852                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
853                    + universal.getReference(),
854                    getDiffModuleContextOfProofLineFormula(i, expected));
855                return ok;
856            }
857        }
858        final RuleKey defined = checker.getRule(universal.getName());
859        if (defined == null) {
860            ok = false;
861            handleProofCheckException(
862                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
863                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
864                + universal.getName(),
865                getCurrentContext());
866            return ok;
867        } else if (!supported.contains(defined.getVersion())) {
868            ok = false;
869            handleProofCheckException(
870                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
871                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
872                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
873                getCurrentContext());
874            return ok;
875        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
876            ok = false;
877            handleProofCheckException(
878                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
879                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
880                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
881                getCurrentContext());
882            return ok;
883        }
884        return ok;
885    }
886 
887    private boolean check(final Existential existential, final int i, final Element element) {
888        final String context = currentContext.getLocationWithinModule();
889        boolean ok = true;
890        final Element reference = getNormalizedLocalProofLineReference(existential.getReference());
891        if (reference == null) {
892            ok = false;
893            setLocationWithinModule(context + ".getReference()");
894            handleProofCheckException(
895                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
896                BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
897                + existential.getReference(),
898                getCurrentContext());
899//        } else if (!lineProved[n.intValue()]) {
900//            ok = false;
901//            setLocationWithinModule(context + ".getReference()");
902//            handleProofCheckException(
903//                BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
904//                BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
905//                + existential.getReference(),
906//                getCurrentContext());
907        } else {
908            final Element current = getNormalizedFormula(element);
909            if (!FormulaUtility.isImplication(current)) {
910                ok = false;
911                setLocationWithinModule(context + ".getReference()");
912                handleProofCheckException(
913                    BasicProofErrors.IMPLICATION_EXPECTED_CODE,
914                    BasicProofErrors.IMPLICATION_EXPECTED_TEXT
915                    + existential.getReference(),
916                    getCurrentContext());
917                return ok;
918            }
919            if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
920                ok = false;
921                setLocationWithinModule(context + ".getSubjectVariable()");
922                handleProofCheckException(
923                    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
924                    BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
925                    getCurrentContext());
926                return ok;
927            }
928            final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
929            final ElementList exi = new DefaultElementList(
930                Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
931            exi.add(existential.getSubjectVariable());
932            exi.add(reference.getList().getElement(0));
933            expected.add(exi);
934            expected.add((reference.getList().getElement(1)));
935            if (!EqualsUtility.equals(current, expected)) {
936                ok = false;
937                handleProofCheckException(
938                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
939                    BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
940                    + existential.getReference(),
941                    getDiffModuleContextOfProofLineFormula(i, expected));
942                return ok;
943            }
944        }
945        final RuleKey defined = checker.getRule(existential.getName());
946        if (defined == null) {
947            ok = false;
948            handleProofCheckException(
949                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
950                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
951                + existential.getName(),
952                getCurrentContext());
953            return ok;
954        } else if (!supported.contains(defined.getVersion())) {
955            ok = false;
956            handleProofCheckException(
957                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
958                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
959                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
960                getCurrentContext());
961            return ok;
962        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
963            ok = false;
964            handleProofCheckException(
965                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
966                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
967                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
968                getCurrentContext());
969            return ok;
970        }
971        return ok;
972    }
973 
974    private boolean check(final ConditionalProof cp, final int i, final Element element) {
975        final ModuleAddress address = currentContext.getModuleLocation();
976        final String context = currentContext.getLocationWithinModule();
977//        System.out.println(getCurrentContext());
978        boolean ok = true;
979        if (cp.getHypothesis() == null || cp.getHypothesis().getFormula() == null
980                || cp.getHypothesis().getFormula().getElement() == null) {
981            ok = false;
982            setLocationWithinModule(context + ".getHypothesis()");
983            handleProofCheckException(
984                BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
985                BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
986                getCurrentContext());
987            return ok;
988        }
989        if (cp.getFormalProofLineList() == null || cp.getFormalProofLineList().size() <= 0) {
990            ok = false;
991            setLocationWithinModule(context + ".getFormalProofLineList()");
992            handleProofCheckException(
993                BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE,
994                BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT,
995                getCurrentContext());
996            return ok;
997        }
998        final ReferenceResolver newResolver = new ReferenceResolver() {
999 
1000            public Element getNormalizedFormula(final Element formula) {
1001                return ProofChecker2Impl.this.getNormalizedFormula(formula);
1002            }
1003 
1004            public Element getNormalizedReferenceFormula(final String reference) {
1005//                System.out.println("Looking for " + reference);
1006                if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1007                    return resolver.getNormalizedFormula(cp.getHypothesis().getFormula()
1008                        .getElement());
1009                }
1010                return ProofChecker2Impl.this.getNormalizedReferenceFormula(reference);
1011            }
1012 
1013            public boolean isProvedFormula(final String reference) {
1014                if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1015                    return true;
1016                }
1017                return ProofChecker2Impl.this.isProvedFormula(reference);
1018            }
1019 
1020            public boolean isLocalProofLineReference(final String reference) {
1021                if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1022                    return true;
1023                }
1024                return ProofChecker2Impl.this.isLocalProofLineReference(reference);
1025            }
1026 
1027            public ModuleContext getReferenceContext(final String reference) {
1028                if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1029                    return new ModuleContext(address, context
1030                        + ".getHypothesis().getLabel()");
1031                }
1032                return ProofChecker2Impl.this.getReferenceContext(reference);
1033            }
1034 
1035            public Element getNormalizedLocalProofLineReference(final String reference) {
1036//                System.out.println("\t resolver looks for " + reference);
1037                if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) {
1038//                    System.out.println("\t resolver found local " + reference);
1039                    return resolver.getNormalizedFormula(
1040                        cp.getHypothesis().getFormula().getElement());
1041                }
1042                return ProofChecker2Impl.this.getNormalizedLocalProofLineReference(reference);
1043            }
1044 
1045        };
1046        final int last = cp.getFormalProofLineList().size() - 1;
1047        setLocationWithinModule(context + ".getFormalProofLineList().get(" + last + ")");
1048        final FormalProofLine line = cp.getFormalProofLineList().get(last);
1049        if (line == null || line.getFormula() == null
1050                || line.getFormula().getElement() == null) {
1051            ok = false;
1052            handleProofCheckException(
1053                BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
1054                BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
1055                getCurrentContext());
1056            return ok;
1057        }
1058        final Element lastFormula = resolver.getNormalizedFormula(line.getFormula().getElement());
1059        final ElementList newConditions = (ElementList) conditions.copy();
1060        // add hypothesis as new condition
1061        newConditions.add(cp.getHypothesis().getFormula().getElement());
1062        setLocationWithinModule(context + ".getFormalProofLineList()");
1063        final LogicalCheckExceptionList eList = (new ProofChecker2Impl()).checkProof(
1064            newConditions, lastFormula, cp.getFormalProofLineList(), checker, getCurrentContext(),
1065            newResolver);
1066        exceptions.add(eList);
1067        ok = eList.size() == 0;
1068        setLocationWithinModule(context + ".getConclusion()");
1069        if (cp.getConclusion() == null || cp.getConclusion().getFormula() == null
1070                || cp.getConclusion().getFormula().getElement() == null) {
1071            ok = false;
1072            handleProofCheckException(
1073                BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
1074                BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
1075                getCurrentContext());
1076            return ok;
1077        }
1078        final Element c = resolver.getNormalizedFormula(cp.getConclusion().getFormula().getElement());
1079        setLocationWithinModule(context + ".getConclusion().getFormula().getElement()");
1080        if (!FormulaUtility.isImplication(c)) {
1081            ok = false;
1082            handleProofCheckException(
1083                BasicProofErrors.IMPLICATION_EXPECTED_CODE,
1084                BasicProofErrors.IMPLICATION_EXPECTED_TEXT,
1085                getCurrentContext());
1086            return ok;
1087        }
1088        final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
1089        expected.add(cp.getHypothesis().getFormula().getElement());
1090        expected.add(lastFormula);
1091//        System.out.println("expected: ");
1092//        ProofFinderUtility.println(cp.getConclusion().getFormula().getElement());
1093        if (!EqualsUtility.equals(cp.getConclusion().getFormula().getElement(), expected)) {
1094//            System.out.println("found: ");
1095//            ProofFinderUtility.println(cp.getConclusion().getFormula().getElement());
1096            ok = false;
1097            handleProofCheckException(
1098                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_CODE,
1099                BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_TEXT,
1100                getDiffModuleContextOfProofLineFormula(i, expected));
1101            return ok;
1102        }
1103        final RuleKey defined = checker.getRule(cp.getName());
1104        if (defined == null) {
1105            ok = false;
1106            handleProofCheckException(
1107                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
1108                BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
1109                + cp.getName(),
1110                getCurrentContext());
1111            return ok;
1112        } else if (!supported.contains(defined.getVersion())) {
1113            ok = false;
1114            handleProofCheckException(
1115                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
1116                BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion()
1117                + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported,
1118                getCurrentContext());
1119            return ok;
1120        } else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) {
1121            ok = false;
1122            handleProofCheckException(
1123                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE,
1124                BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00"
1125                + BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(),
1126                getCurrentContext());
1127            return ok;
1128        }
1129        return ok;
1130    }
1131 
1132    private ModuleContext getModuleContextOfProofLineFormula(final int i) {
1133        if (proof.get(i) instanceof ConditionalProof) {
1134            return new ModuleContext(moduleContext.getModuleLocation(),
1135                    moduleContext.getLocationWithinModule() + ".get(" + i
1136                    + ").getConclusion().getFormula().getElement()");
1137        }
1138        return new ModuleContext(moduleContext.getModuleLocation(),
1139            moduleContext.getLocationWithinModule() + ".get(" + i
1140            + ").getFormula().getElement()");
1141    }
1142 
1143    private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
1144            final Element expected) {
1145        final String diff = FormulaUtility.getDifferenceLocation(
1146            proof.get(i).getFormula().getElement(),  expected);
1147        if (proof.get(i) instanceof ConditionalProof) {
1148            return new ModuleContext(moduleContext.getModuleLocation(),
1149                    moduleContext.getLocationWithinModule() + ".get(" + i
1150                    + ").getConclusion().getFormula().getElement()" + diff);
1151        }
1152        return new ModuleContext(moduleContext.getModuleLocation(),
1153            moduleContext.getLocationWithinModule() + ".get(" + i
1154            + ").getFormula().getElement()" + diff);
1155    }
1156 
1157    /**
1158     * Have we any conditions. If yes we are within an conditional proof argument.
1159     *
1160     * @return  Do we have conditions?
1161     */
1162    private boolean hasConditions() {
1163        return conditions.size() > 0;
1164    }
1165 
1166    private Element getNormalizedProofLine(final Integer n) {
1167        if (n == null) {
1168            return null;
1169        }
1170        int i = n.intValue();
1171        if (i < 0 || i >= proof.size()) {
1172            return null;
1173        }
1174        return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
1175    }
1176 
1177    /**
1178     * Add new {@link ProofCheckException} to exception list.
1179     *
1180     * @param code      Error code.
1181     * @param msg       Error message.
1182     * @param context   Error context.
1183     */
1184    private void handleProofCheckException(final int code, final String msg,
1185            final ModuleContext context) {
1186//        System.out.println(context);
1187//        System.setProperty("qedeq.test.xmlLocationFailures", "true");
1188        final ProofCheckException ex = new ProofCheckException(code, msg, context);
1189        exceptions.add(ex);
1190    }
1191 
1192    /**
1193     * Add new {@link ProofCheckException} to exception list.
1194     *
1195     * @param code              Error code.
1196     * @param msg               Error message.
1197     * @param context           Error context.
1198     * @param referenceContext  Reference context.
1199     */
1200    private void handleProofCheckException(final int code, final String msg,
1201            final ModuleContext context, final ModuleContext referenceContext) {
1202//        System.out.println(context);
1203//        System.setProperty("qedeq.test.xmlLocationFailures", "true");
1204        final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
1205            referenceContext);
1206        exceptions.add(ex);
1207    }
1208 
1209    /**
1210     * Get current context within original.
1211     *
1212     * @return  Current context.
1213     */
1214    protected final ModuleContext getCurrentContext() {
1215        return currentContext;
1216    }
1217 
1218    /**
1219     * Set location information where are we within the original module.
1220     *
1221     * @param   locationWithinModule    Location within module.
1222     */
1223    protected void setLocationWithinModule(final String locationWithinModule) {
1224        getCurrentContext().setLocationWithinModule(locationWithinModule);
1225    }
1226 
1227    public boolean isProvedFormula(final String reference) {
1228        if (label2line.containsKey(reference)) {
1229            return lineProved[((Integer) label2line.get(reference)).intValue()];
1230        }
1231        return resolver.isProvedFormula(reference);
1232    }
1233 
1234    public Element getNormalizedReferenceFormula(final String reference) {
1235//        System.out.println("looking for " + reference);
1236        if (label2line.containsKey(reference)) {
1237//            System.out.println("found in local " + reference);
1238            return getNormalizedProofLine((Integer) label2line.get(reference));
1239        }
1240//        System.out.println("not found in local " + reference);
1241        return resolver.getNormalizedReferenceFormula(reference);
1242    }
1243 
1244    public Element getNormalizedFormula(final Element element) {
1245        return resolver.getNormalizedFormula(element);
1246    }
1247 
1248    public boolean isLocalProofLineReference(final String reference) {
1249        if (label2line.containsKey(reference)) {
1250            return true;
1251        }
1252        return resolver.isLocalProofLineReference(reference);
1253    }
1254 
1255    public Element getNormalizedLocalProofLineReference(final String reference) {
1256//        System.out.println("\t resolver looks for " + reference);
1257        if (label2line.containsKey(reference)) {
1258//            System.out.println("\t resolver found local " + reference);
1259            return getNormalizedProofLine((Integer) label2line.get(reference));
1260        }
1261//        System.out.println("\t resolver asks super resolver for " + reference);
1262        final Element result = resolver.getNormalizedLocalProofLineReference(reference);
1263//        if (result == null) {
1264//            System.out.println("\t super resolver didn't find " + reference);
1265//        } else {
1266//            System.out.println("\t super resolver found " + reference);
1267//        }
1268        return result;
1269    }
1270 
1271    public ModuleContext getReferenceContext(final String reference) {
1272        if (label2line.containsKey(reference)) {
1273            final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
1274                moduleContext.getLocationWithinModule() + ".get("
1275                + label2line.get(reference)
1276                + ").getLabel()");
1277            return lc;
1278        }
1279        return resolver.getReferenceContext(reference);
1280    }
1281 
1282}

[all classes][org.qedeq.kernel.bo.logic.proof.checker]
EMMA 2.1.5320 (stable) (C) Vladimir Roubtsov