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

COVERAGE SUMMARY FOR SOURCE FILE [FormalProofCheckerExecutor.java]

nameclass, %method, %block, %line, %
FormalProofCheckerExecutor.java100% (1/1)79%  (22/28)53%  (578/1089)61%  (136.7/223)

COVERAGE BREAKDOWN BY CLASS AND METHOD

nameclass, %method, %block, %line, %
     
class FormalProofCheckerExecutor100% (1/1)79%  (22/28)53%  (578/1089)61%  (136.7/223)
getNormalizedLocalProofLineReference (String): Element 0%   (0/1)0%   (0/2)0%   (0/1)
getReferenceContext (String): ModuleContext 0%   (0/1)0%   (0/2)0%   (0/1)
visitEnter (FunctionDefinition): void 0%   (0/1)0%   (0/27)0%   (0/7)
visitEnter (PredicateDefinition): void 0%   (0/1)0%   (0/27)0%   (0/7)
visitLeave (FunctionDefinition): void 0%   (0/1)0%   (0/4)0%   (0/2)
visitLeave (PredicateDefinition): void 0%   (0/1)0%   (0/4)0%   (0/2)
getNormalizedFormula (KernelQedeqBo, ElementList): ElementList 100% (1/1)19%  (30/154)34%  (5.8/17)
FormalProofCheckerExecutor (ModuleService, KernelQedeqBo, Parameters): void 100% (1/1)33%  (31/95)48%  (9.2/19)
visitEnter (Axiom): void 100% (1/1)48%  (13/27)57%  (4/7)
visitEnter (InitialFunctionDefinition): void 100% (1/1)48%  (13/27)57%  (4/7)
visitEnter (InitialPredicateDefinition): void 100% (1/1)48%  (13/27)57%  (4/7)
executePlugin (InternalModuleServiceCall, Object): Object 100% (1/1)54%  (89/166)64%  (19.9/31)
visitEnter (Header): void 100% (1/1)55%  (42/77)69%  (9/13)
getRule (String): RuleKey 100% (1/1)57%  (8/14)75%  (3/4)
isProvedFormula (String): boolean 100% (1/1)62%  (63/102)59%  (16/27)
visitEnter (Rule): void 100% (1/1)67%  (54/81)83%  (10/12)
visitEnter (Proposition): void 100% (1/1)82%  (124/152)80%  (24/30)
<static initializer> 100% (1/1)90%  (9/10)90%  (0.9/1)
getNormalizedReferenceFormula (String): Element 100% (1/1)92%  (23/25)80%  (4/5)
addError (ModuleDataException): void 100% (1/1)100% (11/11)100% (4/4)
addError (SourceFileException): void 100% (1/1)100% (11/11)100% (4/4)
getNormalizedFormula (Element): Element 100% (1/1)100% (6/6)100% (1/1)
getNormalizedFormula (KernelQedeqBo, Element): Element 100% (1/1)100% (20/20)100% (5/5)
isLocalProofLineReference (String): boolean 100% (1/1)100% (2/2)100% (1/1)
visitLeave (Axiom): void 100% (1/1)100% (4/4)100% (2/2)
visitLeave (InitialFunctionDefinition): void 100% (1/1)100% (4/4)100% (2/2)
visitLeave (InitialPredicateDefinition): void 100% (1/1)100% (4/4)100% (2/2)
visitLeave (Proposition): void 100% (1/1)100% (4/4)100% (2/2)

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.service.logic;
17 
18 
19import org.qedeq.base.io.Parameters;
20import org.qedeq.base.io.Version;
21import org.qedeq.base.trace.Trace;
22import org.qedeq.base.utility.StringUtility;
23import org.qedeq.kernel.bo.log.QedeqLog;
24import org.qedeq.kernel.bo.logic.ProofCheckerFactoryImpl;
25import org.qedeq.kernel.bo.logic.common.FormulaUtility;
26import org.qedeq.kernel.bo.logic.common.FunctionKey;
27import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
28import org.qedeq.kernel.bo.logic.common.PredicateKey;
29import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
30import org.qedeq.kernel.bo.logic.proof.checker.ProofCheckException;
31import org.qedeq.kernel.bo.logic.proof.common.ProofCheckerFactory;
32import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
33import org.qedeq.kernel.bo.module.InternalModuleServiceCall;
34import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
35import org.qedeq.kernel.bo.module.KernelQedeqBo;
36import org.qedeq.kernel.bo.module.Reference;
37import org.qedeq.kernel.bo.service.basis.ControlVisitor;
38import org.qedeq.kernel.bo.service.basis.ModuleServicePluginExecutor;
39import org.qedeq.kernel.se.base.list.Element;
40import org.qedeq.kernel.se.base.list.ElementList;
41import org.qedeq.kernel.se.base.module.Axiom;
42import org.qedeq.kernel.se.base.module.ChangedRule;
43import org.qedeq.kernel.se.base.module.ChangedRuleList;
44import org.qedeq.kernel.se.base.module.FormalProof;
45import org.qedeq.kernel.se.base.module.FormalProofLineList;
46import org.qedeq.kernel.se.base.module.FunctionDefinition;
47import org.qedeq.kernel.se.base.module.Header;
48import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
49import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
50import org.qedeq.kernel.se.base.module.PredicateDefinition;
51import org.qedeq.kernel.se.base.module.Proposition;
52import org.qedeq.kernel.se.base.module.Rule;
53import org.qedeq.kernel.se.common.CheckLevel;
54import org.qedeq.kernel.se.common.ModuleContext;
55import org.qedeq.kernel.se.common.ModuleDataException;
56import org.qedeq.kernel.se.common.ModuleService;
57import org.qedeq.kernel.se.common.RuleKey;
58import org.qedeq.kernel.se.common.SourceFileException;
59import org.qedeq.kernel.se.common.SourceFileExceptionList;
60import org.qedeq.kernel.se.dto.list.DefaultAtom;
61import org.qedeq.kernel.se.dto.list.DefaultElementList;
62import org.qedeq.kernel.se.state.FormallyProvedState;
63import org.qedeq.kernel.se.visitor.InterruptException;
64 
65 
66/**
67 * Checks if all propositions have a correct formal proof.
68 *
69 * @author  Michael Meyling
70 */
71public final class FormalProofCheckerExecutor extends ControlVisitor implements ModuleServicePluginExecutor,
72        ReferenceResolver, RuleChecker {
73 
74    /** This class. */
75    private static final Class CLASS = FormalProofCheckerExecutor.class;
76 
77    /** Factory for generating new checkers. */
78    private ProofCheckerFactory checkerFactory = null;
79 
80    /** Rule version the module claims to use at maximum. */
81    private Version ruleVersion;
82 
83    /**
84     * Constructor.
85     *
86     * @param   plugin      This plugin we work for.
87     * @param   qedeq       QEDEQ BO object.
88     * @param   parameters  Parameters.
89     */
90    FormalProofCheckerExecutor(final ModuleService plugin, final KernelQedeqBo qedeq,
91            final Parameters parameters) {
92        super(plugin, qedeq);
93        final String method = "FormalProofCheckerExecutor(Plugin, KernelQedeqBo, Map)";
94        final String checkerFactoryClass = parameters.getString("checkerFactory");
95        if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
96            try {
97                Class cl = Class.forName(checkerFactoryClass);
98                checkerFactory = (ProofCheckerFactory) cl.newInstance();
99            } catch (ClassNotFoundException e) {
100                Trace.fatal(CLASS, this, method, "ProofCheckerFactory class not in class path: "
101                    + checkerFactoryClass, e);
102            } catch (InstantiationException e) {
103                Trace.fatal(CLASS, this, method, "ProofCheckerFactory class could not be instanciated: "
104                    + checkerFactoryClass, e);
105            } catch (IllegalAccessException e) {
106                Trace.fatal(CLASS, this, method,
107                    "Programming error, access for instantiation failed for model: "
108                    + checkerFactoryClass, e);
109            } catch (RuntimeException e) {
110                Trace.fatal(CLASS, this, method,
111                    "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
112            }
113        }
114        // fallback is the default checker factory
115        if (checkerFactory == null) {
116            checkerFactory = new ProofCheckerFactoryImpl();
117        }
118    }
119 
120    public Object executePlugin(final InternalModuleServiceCall call, final Object data) throws InterruptException {
121        // we set this as module rule version, and hope it will be changed
122        ruleVersion = new Version("0.00.00");
123        QedeqLog.getInstance().logRequest(
124                "Check logical correctness", getKernelQedeqBo().getUrl());
125        getServices().checkWellFormedness(call.getInternalServiceProcess(), getKernelQedeqBo());
126        if (!getKernelQedeqBo().isWellFormed()) {
127            final String msg = "Check of logical correctness failed";
128            QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
129                "Module is not even well formed.");
130            return Boolean.FALSE;
131        }
132        getKernelQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_EXTERNAL_CHECKING);
133        getKernelQedeqBo().getLabels().resetNodesToProvedUnchecked();
134        final KernelModuleReferenceList list = getKernelQedeqBo().getKernelRequiredModules();
135        for (int i = 0; i < list.size(); i++) {
136            Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
137            getServices().checkFormallyProved(call.getInternalServiceProcess(), list.getKernelQedeqBo(i));
138            if (list.getKernelQedeqBo(i).hasErrors()) {
139                addError(new CheckRequiredModuleException(
140                    LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
141                    LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
142                    + list.getQedeqBo(i).getModuleAddress(),
143                    list.getModuleContext(i)));
144            }
145        }
146        // has at least one import errors?
147        if (getKernelQedeqBo().hasErrors()) {
148            getKernelQedeqBo().setFormallyProvedFailureState(FormallyProvedState.STATE_EXTERNAL_CHECKING_FAILED,
149                getErrorList());
150            final String msg = "Check of logical correctness failed";
151            QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
152                 StringUtility.replace(getKernelQedeqBo().getErrors().getMessage(), "\n", "\n\t"));
153            return Boolean.FALSE;
154        }
155        getKernelQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_INTERNAL_CHECKING);
156        try {
157            traverse(call.getInternalServiceProcess());
158        } catch (SourceFileExceptionList e) {
159            getKernelQedeqBo().setFormallyProvedFailureState(FormallyProvedState.STATE_INTERNAL_CHECKING_FAILED,
160                getErrorList());
161            final String msg = "Check of logical correctness failed";
162            QedeqLog.getInstance().logFailureReply(msg, getKernelQedeqBo().getUrl(),
163                 StringUtility.replace(e.getMessage(), "\n", "\n\t"));
164            return Boolean.FALSE;
165        }
166        getKernelQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_CHECKED);
167        QedeqLog.getInstance().logSuccessfulReply(
168            "Check of logical correctness successful", getKernelQedeqBo().getUrl());
169        return Boolean.TRUE;
170    }
171 
172    public void visitEnter(final Header header) throws ModuleDataException {
173        if (header.getSpecification() == null
174                || header.getSpecification().getRuleVersion() == null) {
175            return;
176        }
177        final String context = getCurrentContext().getLocationWithinModule();
178        setLocationWithinModule(context + ".getSpecification().getRuleVersion()");
179        final String version = header.getSpecification().getRuleVersion().trim();
180        if (!checkerFactory.isRuleVersionSupported(version)) {
181            addError(new ProofCheckException(
182                LogicErrors.RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_CODE,
183                LogicErrors.RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_TEXT + version,
184                getCurrentContext()));
185        } else {
186            try {
187                ruleVersion = new Version(version);
188            } catch (RuntimeException e) {
189                addError(new ProofCheckException(
190                    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
191                    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + version,
192                    getCurrentContext()));
193            }
194        }
195        setLocationWithinModule(context);
196    }
197 
198    public void visitEnter(final Axiom axiom) throws ModuleDataException {
199        if (getNodeBo().isWellFormed()) {
200            getNodeBo().setProved(CheckLevel.SUCCESS);
201        } else {
202            getNodeBo().setProved(CheckLevel.FAILURE);
203            addError(new ProofCheckException(
204                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
205                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
206                getCurrentContext()));
207            return;
208        }
209        setBlocked(true);
210    }
211 
212    public void visitLeave(final Axiom axiom) {
213        setBlocked(false);
214    }
215 
216    public void visitEnter(final PredicateDefinition definition)
217            throws ModuleDataException {
218        if (getNodeBo().isWellFormed()) {
219            getNodeBo().setProved(CheckLevel.SUCCESS);
220        } else {
221            getNodeBo().setProved(CheckLevel.FAILURE);
222            addError(new ProofCheckException(
223                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
224                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
225                getCurrentContext()));
226            return;
227        }
228        setBlocked(true);
229    }
230 
231    public void visitLeave(final PredicateDefinition definition) {
232        setBlocked(false);
233    }
234 
235    public void visitEnter(final InitialPredicateDefinition definition)
236            throws ModuleDataException {
237        if (getNodeBo().isWellFormed()) {
238            getNodeBo().setProved(CheckLevel.SUCCESS);
239        } else {
240            getNodeBo().setProved(CheckLevel.FAILURE);
241            addError(new ProofCheckException(
242                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
243                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
244                getCurrentContext()));
245            return;
246        }
247        setBlocked(true);
248    }
249 
250    public void visitLeave(final InitialPredicateDefinition definition) {
251        setBlocked(false);
252    }
253 
254    public void visitEnter(final InitialFunctionDefinition definition)
255            throws ModuleDataException {
256        if (getNodeBo().isWellFormed()) {
257            getNodeBo().setProved(CheckLevel.SUCCESS);
258        } else {
259            getNodeBo().setProved(CheckLevel.FAILURE);
260            addError(new ProofCheckException(
261                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
262                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
263                getCurrentContext()));
264            return;
265        }
266        setBlocked(true);
267    }
268 
269    public void visitLeave(final InitialFunctionDefinition definition) {
270        setBlocked(false);
271    }
272 
273    public void visitEnter(final FunctionDefinition definition)
274            throws ModuleDataException {
275        if (getNodeBo().isWellFormed()) {
276            getNodeBo().setProved(CheckLevel.SUCCESS);
277        } else {
278            getNodeBo().setProved(CheckLevel.FAILURE);
279            addError(new ProofCheckException(
280                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
281                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
282                getCurrentContext()));
283            return;
284        }
285        setBlocked(true);
286    }
287 
288    public void visitLeave(final FunctionDefinition definition) {
289        setBlocked(false);
290    }
291 
292    public void visitEnter(final Proposition proposition)
293            throws ModuleDataException {
294        // we only check this node, if the well formed check was successful
295        if (!getNodeBo().isWellFormed()) {
296            getNodeBo().setProved(CheckLevel.FAILURE);
297            addError(new ProofCheckException(
298                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
299                LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
300                getCurrentContext()));
301            return;
302        }
303        getNodeBo().setProved(CheckLevel.UNCHECKED);
304        if (proposition.getFormula() == null) {
305            getNodeBo().setProved(CheckLevel.FAILURE);
306            addError(new ProofCheckException(
307                LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_CODE,
308                LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_TEXT,
309                getCurrentContext()));
310            return;
311        }
312        final String context = getCurrentContext().getLocationWithinModule();
313        boolean correctProofFound = false;
314        // we start checking
315        if (proposition.getFormalProofList() != null) {
316            for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
317                final FormalProof proof = proposition.getFormalProofList().get(i);
318                if (proof != null) {
319                    final FormalProofLineList list = proof.getFormalProofLineList();
320                    if (list != null) {
321                        setLocationWithinModule(context + ".getFormalProofList().get("
322                           + i + ").getFormalProofLineList()");
323                        LogicalCheckExceptionList eList
324                            = checkerFactory.createProofChecker(ruleVersion).checkProof(
325                            proposition.getFormula().getElement(), list, this,
326                            getCurrentContext(),
327                            this);
328                        if (!correctProofFound && eList.size() == 0) {
329                            correctProofFound = true;
330                        }
331                        for (int j = 0; j < eList.size(); j++) {
332                            addError(eList.get(j));
333                        }
334                    }
335                }
336            }
337        }
338        setLocationWithinModule(context + ".getFormula()");
339        // only if we found at least one error free formal proof
340        if (correctProofFound) {
341            getNodeBo().setProved(CheckLevel.SUCCESS);
342        } else {
343            getNodeBo().setProved(CheckLevel.FAILURE);
344            addError(new ProofCheckException(
345                LogicErrors.NO_FORMAL_PROOF_FOUND_CODE,
346                LogicErrors.NO_FORMAL_PROOF_FOUND_TEXT,
347                getCurrentContext()));
348        }
349        setBlocked(true);
350    }
351 
352    public void visitLeave(final Proposition definition) {
353        setBlocked(false);
354    }
355 
356    public void visitEnter(final Rule rule) throws ModuleDataException {
357        final String context = getCurrentContext().getLocationWithinModule();
358        // FIXME 20110618 m31: check if this is really a higher version than before?
359        // FIXME 20130413 m31: why we don't use the following method:
360        ///      checkerFactory.createProofChecker(ruleVersion).checkRule
361        getNodeBo().setProved(CheckLevel.UNCHECKED);
362        final ChangedRuleList list = rule.getChangedRuleList();
363        for (int i = 0; list != null && i < list.size(); i++) {
364            setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()");
365            final ChangedRule r = list.get(i);
366            if (!Version.equals(rule.getVersion(), r.getVersion())) {
367                addError(new ProofCheckException(
368                    LogicErrors.OTHER_RULE_VERSION_EXPECTED_CODE,
369                    LogicErrors.OTHER_RULE_VERSION_EXPECTED_TEXT1 + rule.getVersion()
370                    + LogicErrors.OTHER_RULE_VERSION_EXPECTED_TEXT2 + r.getVersion(),
371                    getCurrentContext()));
372            }
373        }
374 
375        if (getNodeBo().isNotProved()) {
376            getNodeBo().setProved(CheckLevel.SUCCESS);
377        } else {
378            getNodeBo().setProved(CheckLevel.FAILURE);
379        }
380    }
381 
382    protected void addError(final ModuleDataException me) {
383        if (getNodeBo() != null) {
384            getNodeBo().setProved(CheckLevel.FAILURE);
385        }
386        super.addError(me);
387    }
388 
389    protected void addError(final SourceFileException me) {
390        if (getNodeBo() != null) {
391            getNodeBo().setProved(CheckLevel.FAILURE);
392        }
393        super.addError(me);
394    }
395 
396    public boolean isProvedFormula(final String reference) {
397        final String method = "hasProvedFormula";
398        final Reference ref = getReference(reference, getCurrentContext(), false, false);
399        if (ref == null) {
400            Trace.info(CLASS, method, "ref == null");
401            return false;
402        }
403        if (ref.isExternalModuleReference()) {
404            Trace.info(CLASS, method, "ref is external module");
405            return false;
406        }
407        if (!ref.isNodeReference()) {
408            Trace.info(CLASS, method, "ref is no node reference");
409            return false;
410        }
411        if (null == ref.getNode()) {
412            Trace.info(CLASS, method, "ref node == null");
413            return false;
414        }
415        if (ref.isSubReference()) {
416            return false;
417        }
418        if (!ref.isProofLineReference()) {
419            if (!ref.getNode().isProved()) {
420                Trace.info(CLASS, method, "ref node is not marked as proved: " + reference);
421            }
422            if (!ref.getNode().isProved()) {
423                return false;
424            }
425            if (!ref.getNode().hasFormula()) {
426                Trace.info(CLASS, method, "node has no formula: " + reference);
427                return false;
428            }
429            return ref.getNode().isProved();
430        }
431        Trace.info(CLASS, method, "proof line references are not ok!");
432        return false;
433    }
434 
435    public Element getNormalizedReferenceFormula(final String reference) {
436        if (!isProvedFormula(reference)) {
437            return null;
438        }
439        final Reference ref = getReference(reference, getCurrentContext(), false, false);
440        final Element formula = ref.getNode().getFormula();
441        return getNormalizedFormula(ref.getNode().getQedeqBo(), formula);
442    }
443 
444    public Element getNormalizedFormula(final Element formula) {
445        return getNormalizedFormula(getKernelQedeqBo(), formula);
446    }
447 
448    private Element getNormalizedFormula(final KernelQedeqBo qedeq, final Element formula) {
449        if (formula == null) {
450            return null;
451        }
452        if (formula.isAtom()) {
453            return new DefaultAtom(formula.getAtom().getString());
454        }
455        return getNormalizedFormula(qedeq, formula.getList());
456    }
457 
458    private ElementList getNormalizedFormula(final KernelQedeqBo qedeq, final ElementList formula) {
459        final ElementList result = new DefaultElementList(formula.getOperator());
460        if (FormulaUtility.isPredicateConstant(formula)) {
461            final PredicateKey key = new PredicateKey(formula.getElement(0).getAtom().getString(),
462                "" + (formula.getList().size() - 1));
463            final DefaultAtom atom = new DefaultAtom(
464                qedeq.getExistenceChecker().get(key).getContext().getModuleLocation().getUrl()
465                + "$" + key.getName());
466            result.add(atom);
467            for (int i = 1; i < formula.size(); i++) {
468                result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
469            }
470        } else if (FormulaUtility.isFunctionConstant(formula)) {
471            final FunctionKey key = new FunctionKey(formula.getElement(0).getAtom().getString(),
472                    "" + (formula.getList().size() - 1));
473            final DefaultAtom atom = new DefaultAtom(
474                qedeq.getExistenceChecker().get(key).getContext().getModuleLocation().getUrl()
475                + "$" + key.getName());
476            result.add(atom);
477            for (int i = 1; i < formula.size(); i++) {
478                result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
479            }
480        } else {
481            for (int i = 0; i < formula.size(); i++) {
482                result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
483            }
484        }
485        return result;
486    }
487 
488    public boolean isLocalProofLineReference(final String reference) {
489        // here we have no proof lines
490        return false;
491    }
492 
493    public ModuleContext getReferenceContext(final String reference) {
494        // here we have no proof lines
495        return null;
496    }
497 
498    public Element getNormalizedLocalProofLineReference(final String reference) {
499        // here we have no proof lines
500        return null;
501    }
502 
503    public RuleKey getRule(final String ruleName) {
504        final RuleKey local = getLocalRuleKey(ruleName);
505        if (local == null) {
506            return getKernelQedeqBo().getExistenceChecker().getParentRuleKey(
507            ruleName);
508        }
509        return local;
510    }
511 
512 
513}

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