001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.logic.proof.checker;
017
018 import java.util.HashMap;
019 import java.util.Map;
020
021 import org.qedeq.base.io.Version;
022 import org.qedeq.base.utility.Enumerator;
023 import org.qedeq.base.utility.EqualsUtility;
024 import org.qedeq.base.utility.StringUtility;
025 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
026 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
027 import org.qedeq.kernel.bo.logic.common.Operators;
028 import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
029 import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
030 import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
031 import org.qedeq.kernel.se.base.list.Element;
032 import org.qedeq.kernel.se.base.list.ElementList;
033 import org.qedeq.kernel.se.base.module.Add;
034 import org.qedeq.kernel.se.base.module.Existential;
035 import org.qedeq.kernel.se.base.module.FormalProofLine;
036 import org.qedeq.kernel.se.base.module.FormalProofLineList;
037 import org.qedeq.kernel.se.base.module.ModusPonens;
038 import org.qedeq.kernel.se.base.module.Reason;
039 import org.qedeq.kernel.se.base.module.Rename;
040 import org.qedeq.kernel.se.base.module.Rule;
041 import org.qedeq.kernel.se.base.module.SubstFree;
042 import org.qedeq.kernel.se.base.module.SubstFunc;
043 import org.qedeq.kernel.se.base.module.SubstPred;
044 import org.qedeq.kernel.se.base.module.Universal;
045 import org.qedeq.kernel.se.common.ModuleContext;
046 import org.qedeq.kernel.se.common.RuleKey;
047 import org.qedeq.kernel.se.dto.list.DefaultElementList;
048 import org.qedeq.kernel.se.dto.list.ElementSet;
049
050
051 /**
052 * Formal proof checker for basic rules.
053 *
054 * @author Michael Meyling
055 */
056 public class ProofChecker1Impl implements ProofChecker {
057
058 /** Proof we want to check. */
059 private FormalProofLineList proof;
060
061 /** Module context of proof line list. */
062 private ModuleContext moduleContext;
063
064 /** Current context. */
065 private ModuleContext currentContext;
066
067 /** Resolver for external references. */
068 private ReferenceResolver resolver;
069
070 /** All exceptions that occurred during checking. */
071 private LogicalCheckExceptionList exceptions;
072
073 /** Array with proof status for each proof line. */
074 private boolean[] lineProved;
075
076 /** Maps local proof line labels to local line number Integers. */
077 private Map label2line;
078
079 /** Rule version we can check. */
080 private final Version ruleVersion;
081
082 /** Rule existence checker. */
083 private RuleChecker checker;
084
085 /**
086 * Constructor.
087 *
088 */
089 public ProofChecker1Impl() {
090 this.ruleVersion = new Version("0.01.00");
091 }
092
093 public LogicalCheckExceptionList checkRule(final Rule rule,
094 final ModuleContext context, final RuleChecker checker,
095 final ReferenceResolver resolver) {
096 exceptions = new LogicalCheckExceptionList();
097 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
098 if (rule.getVersion() == null || !ruleVersion.equals(rule.getVersion())) {
099 final ProofCheckException ex = new ProofCheckException(
100 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
101 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + ruleKey
102 + BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + "{" + ruleVersion + "}",
103 context);
104 exceptions.add(ex);
105 }
106 return exceptions;
107 }
108
109 public LogicalCheckExceptionList checkProof(final Element formula,
110 final FormalProofLineList proof,
111 final RuleChecker checker,
112 final ModuleContext moduleContext,
113 final ReferenceResolver resolver) {
114 this.proof = proof;
115 this.resolver = resolver;
116 this.moduleContext = moduleContext;
117 this.checker = checker;
118 // use copy constructor for changing context
119 currentContext = new ModuleContext(moduleContext);
120 exceptions = new LogicalCheckExceptionList();
121 final String context = moduleContext.getLocationWithinModule();
122 lineProved = new boolean[proof.size()];
123 label2line = new HashMap();
124 for (int i = 0; i < proof.size(); i++) {
125 boolean ok = true;
126 setLocationWithinModule(context + ".get(" + i + ")");
127 final FormalProofLine line = proof.get(i);
128 if (line == null || line.getFormula() == null
129 || line.getFormula().getElement() == null) {
130 ok = false;
131 handleProofCheckException(
132 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE,
133 BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT,
134 getCurrentContext());
135 continue;
136 }
137 setLocationWithinModule(context + ".get(" + i + ").getReason()");
138 final Reason reason = line.getReason();
139 if (reason == null) {
140 ok = false;
141 handleProofCheckException(
142 BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE,
143 BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT,
144 getCurrentContext());
145 continue;
146 }
147 if (line.getLabel() != null && line.getLabel().length() > 0) {
148 final Integer n = (Integer) label2line.get(line.getLabel());
149 if (n != null) {
150 final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(),
151 moduleContext.getLocationWithinModule() + ".get("
152 + ((Integer) label2line.get(line.getLabel()))
153 + ").getLabel()");
154 setLocationWithinModule(context + ".get(" + i + ").getLabel()");
155 handleProofCheckException(
156 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE,
157 BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT
158 + line.getLabel(),
159 getCurrentContext(),
160 lc);
161 }
162 label2line.put(line.getLabel(), new Integer(i));
163 }
164 // check if only basis rules are used
165 // TODO 20110316 m31: this is a dirty trick to get the context of the reason
166 // perhaps we can solve this more elegantly?
167 String getReason = ".get" + StringUtility.getClassName(reason.getClass());
168 if (getReason.endsWith("Vo")) {
169 getReason = getReason.substring(0, getReason.length() - 2) + "()";
170 setLocationWithinModule(context + ".get(" + i + ").getReason()"
171 + getReason);
172 }
173 if (reason instanceof Add) {
174 ok = check((Add) reason, i, line.getFormula().getElement());
175 } else if (reason instanceof Rename) {
176 ok = check((Rename) reason, i, line.getFormula().getElement());
177 } else if (reason instanceof ModusPonens) {
178 ok = check((ModusPonens) reason, i, line.getFormula().getElement());
179 } else if (reason instanceof SubstFree) {
180 ok = check((SubstFree) reason, i, line.getFormula().getElement());
181 } else if (reason instanceof SubstPred) {
182 ok = check((SubstPred) reason, i, line.getFormula().getElement());
183 } else if (reason instanceof SubstFunc) {
184 ok = check((SubstFunc) reason, i, line.getFormula().getElement());
185 } else if (reason instanceof Universal) {
186 ok = check((Universal) reason, i, line.getFormula().getElement());
187 } else if (reason instanceof Existential) {
188 ok = check((Existential) reason, i, line.getFormula().getElement());
189 } else {
190 ok = false;
191 handleProofCheckException(
192 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE,
193 BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
194 + reason.getName(),
195 getCurrentContext());
196 }
197 lineProved[i] = ok;
198 // check if last proof line is identical with proposition formula
199 if (i == proof.size() - 1) {
200 if (!formula.equals(line.getFormula().getElement())) {
201 handleProofCheckException(
202 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE,
203 BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT
204 + reason.getName(),
205 getModuleContextOfProofLineFormula(i));
206 }
207 }
208 }
209 return exceptions;
210 }
211
212 private boolean check(final Add add, final int i, final Element element) {
213 final String context = currentContext.getLocationWithinModule();
214 boolean ok = true;
215 if (add.getReference() == null) {
216 ok = false;
217 setLocationWithinModule(context + ".getReference()");
218 handleProofCheckException(
219 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE,
220 BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT,
221 getCurrentContext());
222 return ok;
223 }
224 if (!resolver.isProvedFormula(add.getReference())) {
225 ok = false;
226 setLocationWithinModule(context + ".getReference()");
227 handleProofCheckException(
228 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
229 BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
230 + add.getReference(),
231 getCurrentContext());
232 return ok;
233 }
234 final Element expected = resolver.getNormalizedReferenceFormula(add.getReference());
235 final Element current = resolver.getNormalizedFormula(element);
236 if (!EqualsUtility.equals(expected, current)) {
237 ok = false;
238 handleProofCheckException(
239 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
240 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
241 + add.getReference(),
242 getDiffModuleContextOfProofLineFormula(i, expected));
243 return ok;
244 }
245 final RuleKey defined = checker.getRule(add.getName());
246 if (defined == null) {
247 ok = false;
248 handleProofCheckException(
249 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
250 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
251 + add.getName(),
252 getCurrentContext());
253 return ok;
254 } else if (!ruleVersion.equals(defined.getVersion())) {
255 ok = false;
256 handleProofCheckException(
257 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
258 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
259 getCurrentContext());
260 return ok;
261 }
262 return ok;
263 }
264
265 private boolean check(final Rename rename, final int i, final Element element) {
266 final String context = currentContext.getLocationWithinModule();
267 boolean ok = true;
268 final Integer n = (Integer) label2line.get(rename.getReference());
269 if (n == null) {
270 ok = false;
271 setLocationWithinModule(context + ".getReference()");
272 handleProofCheckException(
273 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
274 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
275 + rename.getReference(),
276 getCurrentContext());
277 // } else if (!lineProved[n.intValue()]) {
278 // ok = false;
279 // setLocationWithinModule(context + ".getReference()");
280 // handleProofCheckException(
281 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
282 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
283 // + rename.getReference(),
284 // getCurrentContext());
285 } else {
286 final Element f = getNormalizedProofLine(n);
287 final Element expected = FormulaUtility.replaceSubjectVariableQuantifier(
288 rename.getOriginalSubjectVariable(),
289 rename.getReplacementSubjectVariable(), f, rename.getOccurrence(),
290 new Enumerator());
291 final Element current = resolver.getNormalizedFormula(element);
292 if (!EqualsUtility.equals(expected, current)) {
293 ok = false;
294 handleProofCheckException(
295 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
296 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
297 + rename.getReference(),
298 getDiffModuleContextOfProofLineFormula(i, expected));
299 } else {
300 ok = true;
301 }
302 }
303 final RuleKey defined = checker.getRule(rename.getName());
304 if (defined == null) {
305 ok = false;
306 handleProofCheckException(
307 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
308 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
309 + rename.getName(),
310 getCurrentContext());
311 return ok;
312 } else if (!ruleVersion.equals(defined.getVersion())) {
313 ok = false;
314 handleProofCheckException(
315 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
316 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
317 getCurrentContext());
318 return ok;
319 }
320 return ok;
321 }
322
323 private boolean check(final SubstFree substFree, final int i, final Element element) {
324 final String context = currentContext.getLocationWithinModule();
325 boolean ok = true;
326 final Integer n = (Integer) label2line.get(substFree.getReference());
327 if (n == null) {
328 ok = false;
329 setLocationWithinModule(context + ".getReference()");
330 handleProofCheckException(
331 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
332 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
333 + substFree.getReference(),
334 getCurrentContext());
335 // } else if (!lineProved[n.intValue()]) {
336 // ok = false;
337 // setLocationWithinModule(context + ".getReference()");
338 // handleProofCheckException(
339 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
340 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
341 // + substfree.getReference(),
342 // getCurrentContext());
343 } else {
344 final Element f = getNormalizedProofLine(n);
345 final Element current = resolver.getNormalizedFormula(element);
346 final Element expected = f.replace(substFree.getSubjectVariable(),
347 resolver.getNormalizedFormula(substFree.getSubstituteTerm()));
348 if (!EqualsUtility.equals(current, expected)) {
349 ok = false;
350 handleProofCheckException(
351 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
352 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
353 + substFree.getReference(),
354 getDiffModuleContextOfProofLineFormula(i, expected));
355 return ok;
356 }
357 }
358 final RuleKey defined = checker.getRule(substFree.getName());
359 if (defined == null) {
360 ok = false;
361 handleProofCheckException(
362 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
363 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
364 + substFree.getName(),
365 getCurrentContext());
366 return ok;
367 } else if (!ruleVersion.equals(defined.getVersion())) {
368 ok = false;
369 handleProofCheckException(
370 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
371 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
372 getCurrentContext());
373 return ok;
374 }
375 return ok;
376 }
377
378 private boolean check(final SubstPred substPred, final int i, final Element element) {
379 final String context = currentContext.getLocationWithinModule();
380 boolean ok = true;
381 final Integer n = (Integer) label2line.get(substPred.getReference());
382 if (n == null) {
383 ok = false;
384 setLocationWithinModule(context + ".getReference()");
385 handleProofCheckException(
386 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
387 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
388 + substPred.getReference(),
389 getCurrentContext());
390 // } else if (!lineProved[n.intValue()]) {
391 // ok = false;
392 // setLocationWithinModule(context + ".getReference()");
393 // handleProofCheckException(
394 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
395 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
396 // + substpred.getReference(),
397 // getCurrentContext());
398 } else {
399 final Element alpha = getNormalizedProofLine(n);
400 final Element current = resolver.getNormalizedFormula(element);
401 if (substPred.getSubstituteFormula() == null) {
402 ok = false;
403 handleProofCheckException(
404 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
405 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
406 getCurrentContext());
407 return ok;
408 }
409 final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable());
410 final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula());
411 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta);
412 if (!EqualsUtility.equals(current, expected)) {
413 ok = false;
414 handleProofCheckException(
415 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
416 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
417 + substPred.getReference(),
418 getDiffModuleContextOfProofLineFormula(i, expected));
419 return ok;
420 }
421 // check precondition: predicate variable p must have n pairwise different free subject
422 // variables as arguments
423 final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p);
424 if (predFree.size() != p.getList().size() - 1) {
425 ok = false;
426 setLocationWithinModule(context + ".getPredicateVariable()");
427 handleProofCheckException(
428 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
429 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
430 getDiffModuleContextOfProofLineFormula(i, expected));
431 return ok;
432 }
433 for (int j = 1; j < p.getList().size(); j++) {
434 if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) {
435 ok = false;
436 setLocationWithinModule(context + ".getPredicateVariable()");
437 handleProofCheckException(
438 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
439 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
440 getCurrentContext());
441 return ok;
442 }
443 }
444 // check precondition: the free variables of $\beta(x_1, \ldots, x_n)$ without
445 // $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
446 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
447 final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta);
448 if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) {
449 ok = false;
450 setLocationWithinModule(context + ".getSubstituteFormula()");
451 handleProofCheckException(
452 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
453 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
454 getCurrentContext());
455 return ok;
456 }
457 // check precondition: each occurrence of $p(t_1, \ldots, t_n)$ in $\alpha$ contains
458 // no bound variable of $\beta(x_1, \ldots, x_n)$
459 final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta);
460 if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) {
461 ok = false;
462 setLocationWithinModule(context + ".getSubstituteFormula()");
463 handleProofCheckException(
464 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
465 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
466 getCurrentContext());
467 return ok;
468 }
469 // check precondition: resulting formula is well formed was already done by well formed
470 // checker
471 }
472 final RuleKey defined = checker.getRule(substPred.getName());
473 if (defined == null) {
474 ok = false;
475 handleProofCheckException(
476 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
477 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
478 + substPred.getName(),
479 getCurrentContext());
480 return ok;
481 } else if (!ruleVersion.equals(defined.getVersion())) {
482 ok = false;
483 handleProofCheckException(
484 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
485 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
486 getCurrentContext());
487 return ok;
488 }
489 return ok;
490 }
491
492 private boolean check(final SubstFunc substFunc, final int i, final Element element) {
493 final String context = currentContext.getLocationWithinModule();
494 boolean ok = true;
495 final Integer n = (Integer) label2line.get(substFunc.getReference());
496 if (n == null) {
497 ok = false;
498 setLocationWithinModule(context + ".getReference()");
499 handleProofCheckException(
500 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
501 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
502 + substFunc.getReference(),
503 getCurrentContext());
504 // } else if (!lineProved[n.intValue()]) {
505 // ok = false;
506 // setLocationWithinModule(context + ".getReference()");
507 // handleProofCheckException(
508 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
509 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
510 // + substfunc.getReference(),
511 // getCurrentContext());
512 } else {
513 final Element alpha = getNormalizedProofLine(n);
514 final Element current = resolver.getNormalizedFormula(element);
515 if (substFunc.getSubstituteTerm() == null) {
516 ok = false;
517 handleProofCheckException(
518 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE,
519 BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT,
520 getCurrentContext());
521 return ok;
522 }
523 final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable());
524 final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm());
525 final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau);
526 if (!EqualsUtility.equals(current, expected)) {
527 ok = false;
528 handleProofCheckException(
529 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
530 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
531 + substFunc.getReference(),
532 getDiffModuleContextOfProofLineFormula(i, expected));
533 return ok;
534 }
535 // check precondition: function variable $\sigma$ must have n pairwise different free
536 // subject variables as arguments
537 final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma);
538 if (funcFree.size() != sigma.getList().size() - 1) {
539 ok = false;
540 setLocationWithinModule(context + ".getPredicateVariable()");
541 handleProofCheckException(
542 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
543 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
544 getDiffModuleContextOfProofLineFormula(i, expected));
545 return ok;
546 }
547 for (int j = 1; j < sigma.getList().size(); j++) {
548 if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) {
549 ok = false;
550 setLocationWithinModule(context + ".getPredicateVariable()");
551 handleProofCheckException(
552 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE,
553 BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT,
554 getCurrentContext());
555 return ok;
556 }
557 }
558 // check precondition: the free variables of $\tau(x_1, \ldots, x_n)$
559 // without $x_1$, \ldots, $x_n$ do not occur as bound variables in $\alpha$
560 final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha);
561 final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau);
562 if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) {
563 ok = false;
564 setLocationWithinModule(context + ".getSubstituteFormula()");
565 handleProofCheckException(
566 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE,
567 BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT,
568 getCurrentContext());
569 return ok;
570 }
571 // check precondition: each occurrence of $\sigma(t_1, \ldots, t_n)$ in $\alpha$
572 // contains no bound variable of $\tau(x_1, \ldots, x_n)$
573 final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau);
574 if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) {
575 ok = false;
576 setLocationWithinModule(context + ".getSubstituteFormula()");
577 handleProofCheckException(
578 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE,
579 BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT,
580 getCurrentContext());
581 return ok;
582 }
583 // check precondition: resulting formula is well formed was already done by well formed
584 // checker
585 }
586 final RuleKey defined = checker.getRule(substFunc.getName());
587 if (defined == null) {
588 ok = false;
589 handleProofCheckException(
590 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
591 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
592 + substFunc.getName(),
593 getCurrentContext());
594 return ok;
595 } else if (!ruleVersion.equals(defined.getVersion())) {
596 ok = false;
597 handleProofCheckException(
598 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
599 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
600 getCurrentContext());
601 return ok;
602 }
603 return ok;
604 }
605
606 private boolean check(final ModusPonens mp, final int i, final Element element) {
607 final String context = currentContext.getLocationWithinModule();
608 boolean ok = true;
609 final Integer n1 = (Integer) label2line.get(mp.getReference1());
610 if (n1 == null) {
611 ok = false;
612 setLocationWithinModule(context + ".getReference1()");
613 handleProofCheckException(
614 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
615 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
616 + mp.getReference1(),
617 getCurrentContext());
618 // } else if (!lineProved[n1.intValue()]) {
619 // ok = false;
620 // setLocationWithinModule(context + ".getReference1()");
621 // handleProofCheckException(
622 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
623 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
624 // + mp.getReference1(),
625 // getCurrentContext());
626 }
627 final Integer n2 = (Integer) label2line.get(mp.getReference2());
628 if (n2 == null) {
629 ok = false;
630 setLocationWithinModule(context + ".getReference2()");
631 handleProofCheckException(
632 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
633 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
634 + mp.getReference2(),
635 getCurrentContext());
636 // } else if (!lineProved[n2.intValue()]) {
637 // ok = false;
638 // setLocationWithinModule(context + ".getReference2()");
639 // handleProofCheckException(
640 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
641 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
642 // + mp.getReference1(),
643 // getCurrentContext());
644 }
645 if (ok) {
646 final Element f1 = getNormalizedProofLine(n1);
647 final Element f2 = getNormalizedProofLine(n2);
648 final Element current = getNormalizedProofLine(i);
649 if (!FormulaUtility.isImplication(f1)) {
650 ok = false;
651 setLocationWithinModule(context + ".getReference1()");
652 handleProofCheckException(
653 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
654 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
655 + mp.getReference1(),
656 getCurrentContext());
657 } else if (!f2.equals(f1.getList().getElement(0))) {
658 ok = false;
659 setLocationWithinModule(context + ".getReference2()");
660 handleProofCheckException(
661 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE,
662 BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
663 + mp.getReference2(),
664 getCurrentContext(),
665 getModuleContextOfProofLineFormula(n1.intValue()));
666 } else if (!current.equals(f1.getList().getElement(1))) {
667 ok = false;
668 setLocationWithinModule(context + ".getReference1()");
669 handleProofCheckException(
670 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE,
671 BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT
672 + mp.getReference1(),
673 getCurrentContext(),
674 getModuleContextOfProofLineFormula(n1.intValue()));
675 } else {
676 ok = true;
677 }
678 }
679 final RuleKey defined = checker.getRule(mp.getName());
680 if (defined == null) {
681 ok = false;
682 handleProofCheckException(
683 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
684 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
685 + mp.getName(),
686 getCurrentContext());
687 return ok;
688 } else if (!ruleVersion.equals(defined.getVersion())) {
689 ok = false;
690 handleProofCheckException(
691 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
692 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
693 getCurrentContext());
694 return ok;
695 }
696 return ok;
697 }
698
699 private boolean check(final Universal universal, final int i, final Element element) {
700 final String context = currentContext.getLocationWithinModule();
701 boolean ok = true;
702 final Integer n = (Integer) label2line.get(universal.getReference());
703 if (n == null) {
704 ok = false;
705 setLocationWithinModule(context + ".getReference()");
706 handleProofCheckException(
707 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
708 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
709 + universal.getReference(),
710 getCurrentContext());
711 // } else if (!lineProved[n.intValue()]) {
712 // ok = false;
713 // setLocationWithinModule(context + ".getReference()");
714 // handleProofCheckException(
715 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
716 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
717 // + universal.getReference(),
718 // getCurrentContext());
719 } else {
720 final Element f = getNormalizedProofLine(n);
721 final Element current = resolver.getNormalizedFormula(element);
722 if (!FormulaUtility.isImplication(f)) {
723 ok = false;
724 setLocationWithinModule(context + ".getReference()");
725 handleProofCheckException(
726 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
727 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
728 + universal.getReference(),
729 getCurrentContext());
730 return ok;
731 }
732 if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) {
733 ok = false;
734 setLocationWithinModule(context + ".getSubjectVariable()");
735 handleProofCheckException(
736 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
737 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
738 getCurrentContext());
739 return ok;
740 }
741 final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
742 expected.add((f.getList().getElement(0)));
743 final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR);
744 uni.add(universal.getSubjectVariable());
745 uni.add(f.getList().getElement(1));
746 expected.add(uni);
747 if (!EqualsUtility.equals(current, expected)) {
748 ok = false;
749 handleProofCheckException(
750 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
751 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
752 + universal.getReference(),
753 getDiffModuleContextOfProofLineFormula(i, expected));
754 return ok;
755 }
756 }
757 final RuleKey defined = checker.getRule(universal.getName());
758 if (defined == null) {
759 ok = false;
760 handleProofCheckException(
761 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
762 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
763 + universal.getName(),
764 getCurrentContext());
765 return ok;
766 } else if (!ruleVersion.equals(defined.getVersion())) {
767 ok = false;
768 handleProofCheckException(
769 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
770 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
771 getCurrentContext());
772 return ok;
773 }
774 return ok;
775 }
776
777 private boolean check(final Existential existential, final int i, final Element element) {
778 final String context = currentContext.getLocationWithinModule();
779 boolean ok = true;
780 final Integer n = (Integer) label2line.get(existential.getReference());
781 if (n == null) {
782 ok = false;
783 setLocationWithinModule(context + ".getReference()");
784 handleProofCheckException(
785 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE,
786 BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
787 + existential.getReference(),
788 getCurrentContext());
789 // } else if (!lineProved[n.intValue()]) {
790 // ok = false;
791 // setLocationWithinModule(context + ".getReference()");
792 // handleProofCheckException(
793 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE,
794 // BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
795 // + existential.getReference(),
796 // getCurrentContext());
797 } else {
798 final Element f = getNormalizedProofLine(n);
799 final Element current = resolver.getNormalizedFormula(element);
800 if (!FormulaUtility.isImplication(f)) {
801 ok = false;
802 setLocationWithinModule(context + ".getReference()");
803 handleProofCheckException(
804 BasicProofErrors.IMPLICATION_EXPECTED_CODE,
805 BasicProofErrors.IMPLICATION_EXPECTED_TEXT
806 + existential.getReference(),
807 getCurrentContext());
808 return ok;
809 }
810 if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) {
811 ok = false;
812 setLocationWithinModule(context + ".getSubjectVariable()");
813 handleProofCheckException(
814 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE,
815 BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT,
816 getCurrentContext());
817 return ok;
818 }
819 final DefaultElementList expected = new DefaultElementList(f.getList().getOperator());
820 final ElementList exi = new DefaultElementList(
821 Operators.EXISTENTIAL_QUANTIFIER_OPERATOR);
822 exi.add(existential.getSubjectVariable());
823 exi.add(f.getList().getElement(0));
824 expected.add(exi);
825 expected.add((f.getList().getElement(1)));
826 if (!EqualsUtility.equals(current, expected)) {
827 ok = false;
828 handleProofCheckException(
829 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE,
830 BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT
831 + existential.getReference(),
832 getDiffModuleContextOfProofLineFormula(i, expected));
833 return ok;
834 }
835 }
836 final RuleKey defined = checker.getRule(existential.getName());
837 if (defined == null) {
838 ok = false;
839 handleProofCheckException(
840 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE,
841 BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
842 + existential.getName(),
843 getCurrentContext());
844 return ok;
845 } else if (!ruleVersion.equals(defined.getVersion())) {
846 ok = false;
847 handleProofCheckException(
848 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE,
849 BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion(),
850 getCurrentContext());
851 return ok;
852 }
853 return ok;
854 }
855
856 private ModuleContext getModuleContextOfProofLineFormula(final int i) {
857 return new ModuleContext(moduleContext.getModuleLocation(),
858 moduleContext.getLocationWithinModule() + ".get(" + i
859 + ").getFormula().getElement()");
860 }
861
862 private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,
863 final Element expected) {
864 final String diff = FormulaUtility.getDifferenceLocation(
865 proof.get(i).getFormula().getElement(), expected);
866 return new ModuleContext(moduleContext.getModuleLocation(),
867 moduleContext.getLocationWithinModule() + ".get(" + i
868 + ").getFormula().getElement()" + diff);
869 }
870
871 private Element getNormalizedProofLine(final Integer n) {
872 if (n == null) {
873 return null;
874 }
875 return getNormalizedProofLine(n.intValue());
876 }
877
878 private Element getNormalizedProofLine(final int i) {
879 if (i < 0 || i >= proof.size()) {
880 return null;
881 }
882 return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement());
883 }
884
885 /**
886 * Add new {@link ProofCheckException} to exception list.
887 *
888 * @param code Error code.
889 * @param msg Error message.
890 * @param context Error context.
891 */
892 private void handleProofCheckException(final int code, final String msg,
893 final ModuleContext context) {
894 // System.out.println(context);
895 // System.setProperty("qedeq.test.xmlLocationFailures", "true");
896 final ProofCheckException ex = new ProofCheckException(code, msg, context);
897 exceptions.add(ex);
898 }
899
900 /**
901 * Add new {@link ProofCheckException} to exception list.
902 *
903 * @param code Error code.
904 * @param msg Error message.
905 * @param context Error context.
906 * @param referenceContext Reference context.
907 */
908 private void handleProofCheckException(final int code, final String msg,
909 final ModuleContext context, final ModuleContext referenceContext) {
910 // System.out.println(context);
911 // System.setProperty("qedeq.test.xmlLocationFailures", "true");
912 final ProofCheckException ex = new ProofCheckException(code, msg, null, context,
913 referenceContext);
914 exceptions.add(ex);
915 }
916
917 /**
918 * Set location information where are we within the original module.
919 *
920 * @param locationWithinModule Location within module.
921 */
922 protected void setLocationWithinModule(final String locationWithinModule) {
923 getCurrentContext().setLocationWithinModule(locationWithinModule);
924 }
925
926 /**
927 * Get current context within original.
928 *
929 * @return Current context.
930 */
931 protected final ModuleContext getCurrentContext() {
932 return currentContext;
933 }
934
935
936 }
|