01 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
02 *
03 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
04 *
05 * "Hilbert II" is free software; you can redistribute
06 * it and/or modify it under the terms of the GNU General Public
07 * License as published by the Free Software Foundation; either
08 * version 2 of the License, or (at your option) any later version.
09 *
10 * This program is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 */
15
16 package org.qedeq.kernel.bo.logic.proof.checker;
17
18 import org.qedeq.base.io.Version;
19 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
20 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
21 import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
22 import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
23 import org.qedeq.kernel.se.base.list.Element;
24 import org.qedeq.kernel.se.base.module.FormalProofLineList;
25 import org.qedeq.kernel.se.base.module.Rule;
26 import org.qedeq.kernel.se.common.ModuleContext;
27
28
29 /**
30 * Formal proof checker that don't allow any proof method.
31 *
32 * @author Michael Meyling
33 */
34 public class ProofChecker0Impl implements ProofChecker {
35
36 /** Rule version we can check. */
37 private final Version ruleVersion;
38
39 /**
40 * Constructor.
41 *
42 */
43 public ProofChecker0Impl() {
44 this.ruleVersion = new Version("0.00.00");
45 }
46
47 public LogicalCheckExceptionList checkProof(final Element formula,
48 final FormalProofLineList proof,
49 final RuleChecker checker,
50 final ModuleContext moduleContext,
51 final ReferenceResolver resolver) {
52 final ProofCheckException ex = new ProofCheckException(
53 BasicProofErrors.NO_FORMAL_PROOFS_SUPORTED_CODE,
54 BasicProofErrors.NO_FORMAL_PROOFS_SUPORTED_TEXT + ruleVersion,
55 null, moduleContext, null);
56 final LogicalCheckExceptionList exceptions = new LogicalCheckExceptionList();
57 exceptions.add(ex);
58 return exceptions;
59 }
60
61 public LogicalCheckExceptionList checkRule(final Rule rule,
62 final ModuleContext context, final RuleChecker checker,
63 final ReferenceResolver resolver) {
64 // we just ignore rule definitions
65 final LogicalCheckExceptionList exceptions = new LogicalCheckExceptionList();
66 return exceptions;
67 }
68
69 }
|