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.finder;
017
018 import java.util.ArrayList;
019 import java.util.Iterator;
020 import java.util.List;
021 import java.util.SortedSet;
022 import java.util.TreeSet;
023
024 import org.qedeq.base.io.Parameters;
025 import org.qedeq.base.utility.StringUtility;
026 import org.qedeq.kernel.bo.common.Element2Utf8;
027 import org.qedeq.kernel.bo.log.ModuleLogListener;
028 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
029 import org.qedeq.kernel.bo.logic.common.Operators;
030 import org.qedeq.kernel.bo.logic.proof.common.ProofException;
031 import org.qedeq.kernel.bo.logic.proof.common.ProofFinder;
032 import org.qedeq.kernel.bo.logic.proof.common.ProofFoundException;
033 import org.qedeq.kernel.bo.logic.proof.common.ProofNotFoundException;
034 import org.qedeq.kernel.se.base.list.Element;
035 import org.qedeq.kernel.se.base.list.ElementList;
036 import org.qedeq.kernel.se.base.module.Add;
037 import org.qedeq.kernel.se.base.module.FormalProofLineList;
038 import org.qedeq.kernel.se.base.module.ModusPonens;
039 import org.qedeq.kernel.se.base.module.Reason;
040 import org.qedeq.kernel.se.common.ModuleContext;
041 import org.qedeq.kernel.se.dto.list.DefaultElementList;
042 import org.qedeq.kernel.se.dto.list.ElementSet;
043 import org.qedeq.kernel.se.visitor.InterruptException;
044
045
046 /**
047 * Find basic proofs for formulas.
048 *
049 * @author Michael Meyling
050 */
051 public class ProofFinderImpl implements ProofFinder {
052
053 /** List of proof lines. */
054 private List lines;
055
056 /** List of reasons. */
057 private List reasons;
058
059 /** Set of all predicate variables that occur in this proof anywhere. */
060 private ElementSet allPredVars;
061
062 /** Set of all substitution formulas we try. */
063 private ElementSet partGoalFormulas;
064
065 /** Below this number MP was tried. */
066 private int mpLast;
067
068 /** Goal to prove. */
069 private Element goalFormula;
070
071 /** Number of extra propositional variables. */
072 private int extraVars;
073
074 /** Skip this number list of formulas. */
075 private String skipFormulas;
076
077 /** Log proof line after this number of new proof lines. */
078 private int logFrequence;
079
080 /** Ordered substitution methods that implement {@link Substitute}. */
081 private SortedSet substitutionMethods;
082
083 /** Maximum number of proof lines. */
084 private int maxProofLines;
085
086 /** Here are we. */
087 private ModuleContext context;
088
089 /** Log progress herein. */
090 private ModuleLogListener log;
091
092 /** Transformer to get UTF-8 out of formulas. */
093 private Element2Utf8 trans;
094
095 /**
096 * Constructor.
097 */
098 public ProofFinderImpl() {
099 // nothing to do
100 }
101
102 public void findProof(final Element formula,
103 final FormalProofLineList proof, final ModuleContext context,
104 final Parameters parameters, final ModuleLogListener log, final Element2Utf8 trans)
105 throws ProofException, InterruptException {
106 this.goalFormula = formula;
107 this.context = new ModuleContext(context); // use copy constructor to fix it
108 this.log = log;
109 this.trans = trans;
110 substitutionMethods = new TreeSet();
111 extraVars = parameters.getInt("extraVars");
112 maxProofLines = parameters.getInt("maximumProofLines");
113 skipFormulas = parameters.getString("skipFormulas").trim();
114 if (skipFormulas.length() > 0) {
115 log.logMessageState("skipping the following formula numbers: " + skipFormulas);
116 skipFormulas = "," + StringUtility.replace(skipFormulas, " ", "") + ",";
117 }
118 // TODO 20110606 m31: check that we have the correct format (e.g. only "," as separator)
119 System.out.println("maximumProofLines = " + maxProofLines);
120 int weight = 0;
121 weight = parameters.getInt("propositionVariableWeight");
122 if (weight > 0) {
123 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("propositionVariableOrder")) {
124 public void substitute(final int i) throws ProofException {
125 substituteByPropositionVariables(i);
126 }
127 });
128 }
129 weight = parameters.getInt("partFormulaWeight");
130 if (weight > 0) {
131 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("partFormulaOrder")) {
132 public void substitute(final int i) throws ProofException {
133 substitutePartGoalFormulas(i);
134 }
135 });
136 }
137 weight = parameters.getInt("disjunctionWeight");
138 if (weight > 0) {
139 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("disjunctionOrder")) {
140 public void substitute(final int i) throws ProofException {
141 substituteDisjunction(i);
142 }
143 });
144 }
145 weight = parameters.getInt("implicationWeight");
146 if (weight > 0) {
147 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("implicationOrder")) {
148 public void substitute(final int i) throws ProofException {
149 substituteImplication(i);
150 }
151 });
152 }
153 weight = parameters.getInt("negationWeight");
154 if (weight > 0) {
155 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("negationOrder")) {
156 public void substitute(final int i) throws ProofException {
157 substituteNegation(i);
158 }
159 });
160 }
161 weight = parameters.getInt("conjunctionWeight");
162 if (weight > 0) {
163 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("conjunctionOrder")) {
164 public void substitute(final int i) throws ProofException {
165 substituteConjunction(i);
166 }
167 });
168 }
169 weight = parameters.getInt("equivalenceWeight");
170 if (weight > 0) {
171 substitutionMethods.add(new SubstituteBase(weight, parameters.getInt("equivalenceOrder")) {
172 public void substitute(final int i) throws ProofException {
173 substituteEquivalence(i);
174 }
175 });
176 }
177 logFrequence = parameters.getInt("logFrequence");
178
179 lines = new ArrayList();
180 reasons = new ArrayList();
181 setAllPredVars(proof);
182 partGoalFormulas = FormulaUtility.getPartFormulas(goalFormula);
183 log.logMessageState("our goal: " + trans.getUtf8(formula));
184 int size2 = 0;
185 while (true) {
186 // check if the thread should be interrupted
187 if (Thread.interrupted()) {
188 throw new InterruptException(this.context);
189 }
190 int size1 = lines.size();
191 tryModusPonensAll();
192 final Iterator iter = substitutionMethods.iterator();
193 while (iter.hasNext()) {
194 final Substitute method = (Substitute) iter.next();
195 // System.out.println(method.getClass());
196 for (int j = 0; j < method.getWeight(); j++) {
197 if (method.nextLine() >= lines.size()) {
198 break;
199 }
200 method.substitute();
201 tryModusPonensAll();
202 }
203 }
204 // System.out.println(lines.size());
205 if (size2 == lines.size()) {
206 // we didn't generate new lines, so we just quit
207 log.logMessageState(FinderErrors.PROOF_NOT_FOUND_TEXT + size2);
208 throw new ProofNotFoundException(FinderErrors.PROOF_NOT_FOUND_CODE,
209 FinderErrors.PROOF_NOT_FOUND_TEXT + size2, context);
210 }
211 size2 = size1;
212 }
213 }
214
215 private void setAllPredVars(final FormalProofLineList proof) {
216 log.logMessageState("using the following formulas:");
217 allPredVars = new ElementSet();
218 // add all "add" proof formulas to our proof line list
219 for (int i = 0; i < proof.size(); i++) {
220 // should we skip this formula
221 if (skipFormulas.indexOf("," + (i + 1) + ",") >= 0) {
222 continue;
223 }
224 final Reason reason = proof.get(i).getReason();
225 if (!(reason instanceof Add)) {
226 continue;
227 }
228 final Element formula = proof.get(i).getFormula().getElement();
229 lines.add(formula);
230 reasons.add(reason);
231 log.logMessageState(ProofFinderUtility.getUtf8Line(formula, reason, i, trans));
232 allPredVars.union(FormulaUtility.getPropositionVariables(
233 formula));
234 }
235 String max = "A";
236 final Iterator iter = allPredVars.iterator();
237 while (iter.hasNext()) {
238 final ElementList v = (ElementList) iter.next();
239 final String name = v.getElement(0).getAtom().getString();
240 if (-1 == max.compareTo(name)) {
241 max = name;
242 }
243 }
244 System.out.println("Adding extra variables:");
245 for (int i = 1; i <= extraVars; i++) {
246 max = (char) (max.charAt(0) + i) + "";
247 System.out.println("\t" + max);
248 // add extra predicate variable
249 allPredVars.add(FormulaUtility.createPredicateVariable(max));
250 }
251 }
252
253 /**
254 * Try all Modus Ponens with all new lines. Remember tested maximum.
255 *
256 * @throws ProofException Proof found, or limits exceeded.
257 */
258 private void tryModusPonensAll() throws ProofException {
259 int until = lines.size();
260 for (int i = 0; i < until; i++) {
261 final Element first = (Element) lines.get(i);
262 if (!FormulaUtility.isImplication(first)) {
263 continue;
264 }
265 for (int j = (i < mpLast ? mpLast : 0); j < until; j++) {
266 if (first.getList().getElement(0).equals(
267 lines.get(j))) {
268 final ModusPonens mp = new ModusPonensBo(i, j);
269 addFormula(first.getList().getElement(1), mp);
270 }
271 }
272 }
273 mpLast = until;
274 }
275
276 /**
277 * Make all possible substitutions by propositional variables in a proof line.
278 *
279 * @param i Proof line number we want to try substitution.
280 * @throws ProofException We found a proof or have to end the search!
281 */
282 private void substituteByPropositionVariables(final int i) throws ProofException {
283 final Element f = (Element) lines.get(i);
284 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
285 final Iterator iter = vars.iterator();
286 while (iter.hasNext()) {
287 final ElementList var = (ElementList) iter.next();
288 final Iterator all = allPredVars.iterator();
289 while (all.hasNext()) {
290 final ElementList subst = (ElementList) all.next();
291 if (var.equals(subst)) {
292 continue;
293 }
294 final Element created = FormulaUtility.replaceOperatorVariable(
295 f, var, subst);
296 addFormula(created, new SubstPredBo(i, var, subst));
297 }
298 }
299 }
300
301 /**
302 * Make all substitutions by part goal formulas in a proof line.
303 *
304 * @param i Proof line number we want to try substitution.
305 * @throws ProofException We found a proof or have to end the search!
306 */
307 private void substitutePartGoalFormulas(final int i) throws ProofException {
308 final Element f = (Element) lines.get(i);
309 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
310 final Iterator iter = vars.iterator();
311 while (iter.hasNext()) {
312 final ElementList var = (ElementList) iter.next();
313 {
314 final Iterator all = partGoalFormulas.iterator();
315 while (all.hasNext()) {
316 final ElementList subst = (ElementList) all.next();
317 if (var.equals(subst)) {
318 continue;
319 }
320 final Element created = FormulaUtility.replaceOperatorVariable(
321 f, var, subst);
322 addFormula(created, new SubstPredBo(i, var, subst));
323 }
324 }
325 }
326 }
327
328 /**
329 * Make all substitutions by negation in a proof line.
330 *
331 * @param i Proof line number we want to try substitution.
332 * @throws ProofException We found a proof or have to end the search!
333 */
334 private void substituteNegation(final int i) throws ProofException {
335 final Element f = (Element) lines.get(i);
336 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
337 final Iterator iter = vars.iterator();
338 while (iter.hasNext()) {
339 final ElementList var = (ElementList) iter.next();
340 final Iterator all = allPredVars.iterator();
341 while (all.hasNext()) {
342 final ElementList var2 = (ElementList) all.next();
343 final ElementList subst = new DefaultElementList(Operators.NEGATION_OPERATOR);
344 subst.add(var2);
345 final Element created = FormulaUtility.replaceOperatorVariable(
346 f, var, subst);
347 addFormula(created, new SubstPredBo(i, var, subst));
348 }
349 }
350 }
351
352 /**
353 * Make all substitutions by conjunction in a proof line.
354 *
355 * @param i Proof line number we want to try substitution.
356 * @throws ProofException We found a proof or have to end the search!
357 */
358 private void substituteConjunction(final int i) throws ProofException {
359 final Element f = (Element) lines.get(i);
360 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
361 final Iterator iter = vars.iterator();
362 while (iter.hasNext()) {
363 final ElementList var = (ElementList) iter.next();
364 createReplacement(i, f, var, Operators.CONJUNCTION_OPERATOR, true);
365 createReplacement(i, f, var, Operators.CONJUNCTION_OPERATOR, false);
366 }
367 }
368
369 /**
370 * Make all substitutions by disjunction in a proof line.
371 *
372 * @param i Proof line number we want to try substitution.
373 * @throws ProofException We found a proof or have to end the search!
374 */
375 private void substituteDisjunction(final int i) throws ProofException {
376 final Element f = (Element) lines.get(i);
377 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
378 final Iterator iter = vars.iterator();
379 while (iter.hasNext()) {
380 final ElementList var = (ElementList) iter.next();
381 createReplacement(i, f, var, Operators.DISJUNCTION_OPERATOR, true);
382 createReplacement(i, f, var, Operators.DISJUNCTION_OPERATOR, false);
383 }
384 }
385
386 /**
387 * Make all substitutions by implication in a proof line.
388 *
389 * @param i Proof line number we want to try substitution.
390 * @throws ProofException We found a proof or have to end the search!
391 */
392 private void substituteImplication(final int i) throws ProofException {
393 final Element f = (Element) lines.get(i);
394 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
395 final Iterator iter = vars.iterator();
396 while (iter.hasNext()) {
397 final ElementList var = (ElementList) iter.next();
398 createReplacement(i, f, var, Operators.IMPLICATION_OPERATOR, true);
399 createReplacement(i, f, var, Operators.IMPLICATION_OPERATOR, false);
400 }
401 }
402
403 /**
404 * Make all substitutions by equivalence in a proof line.
405 *
406 * @param i Proof line number we want to try substitution.
407 * @throws ProofException We found a proof or have to end the search!
408 */
409 private void substituteEquivalence(final int i) throws ProofException {
410 final Element f = (Element) lines.get(i);
411 final ElementSet vars = FormulaUtility.getPropositionVariables(f);
412 final Iterator iter = vars.iterator();
413 while (iter.hasNext()) {
414 final ElementList var = (ElementList) iter.next();
415 createReplacement(i, f, var, Operators.EQUIVALENCE_OPERATOR, true);
416 createReplacement(i, f, var, Operators.EQUIVALENCE_OPERATOR, false);
417 }
418 }
419
420 /**
421 * Substitute predicate variable <code>var</code> by binary operator with old variable
422 * and new variable and add this as a new proof line.
423 *
424 * @param i Proof line number we work on.
425 * @param f Proof line formula.
426 * @param var Predicate variable we want to replace.
427 * @param operator Operator of replacement formula.
428 * @param left Is old variable at left hand of new operator?
429 * @throws ProofException We found a proof or have to end the search!
430 */
431 private void createReplacement(final int i, final Element f,
432 final ElementList var, final String operator, final boolean left) throws ProofException {
433 final Iterator a = allPredVars.iterator();
434 while (a.hasNext()) {
435 final ElementList var2 = (ElementList) a.next();
436 final ElementList subst = new DefaultElementList(operator);
437 if (left) {
438 subst.add(var);
439 subst.add(var2);
440 } else {
441 subst.add(var2);
442 subst.add(var);
443 }
444 final Element created = FormulaUtility.replaceOperatorVariable(
445 f, var, subst);
446 addFormula(created, new SubstPredBo(i, var, subst));
447 }
448 }
449
450 private void addFormula(final Element formula, final Reason reason) throws ProofException {
451 if (!lines.contains(formula)) {
452 lines.add(formula);
453 reasons.add(reason);
454 // printLine(lines.size() - 1);
455 if (goalFormula.equals(formula)) {
456 final int size = lines.size();
457 log.logMessageState(FinderErrors.PROOF_FOUND_TEXT + size);
458 throw new ProofFoundException(FinderErrors.PROOF_FOUND_CODE,
459 FinderErrors.PROOF_FOUND_TEXT + size,
460 ProofFinderUtility.shortenProof(lines, reasons, log, trans), context);
461 }
462 // did we reach our maximum?
463 if (lines.size() >= maxProofLines) {
464 final int size = lines.size();
465 if (logFrequence > 0) {
466 log.logMessageState(ProofFinderUtility.getUtf8Line(lines, reasons, lines.size() - 1,
467 trans));
468 }
469 log.logMessageState(FinderErrors.PROOF_NOT_FOUND_TEXT + size);
470 throw new ProofNotFoundException(FinderErrors.PROOF_NOT_FOUND_CODE,
471 FinderErrors.PROOF_NOT_FOUND_TEXT + size, context);
472 }
473 if (logFrequence > 0 && (lines.size() - 1) % logFrequence == 0) {
474 log.logMessageState(ProofFinderUtility.getUtf8Line(lines, reasons, lines.size() - 1,
475 trans));
476 }
477 }
478 }
479
480 public String getExecutionActionDescription() {
481 return ProofFinderUtility.getUtf8Line(lines, reasons, lines.size() - 1, trans);
482 }
483
484 /**
485 * These is the basis implementation for substitution methods.
486 */
487 private abstract class SubstituteBase implements Substitute {
488
489 /** Next proof line we will work on. */
490 private int next = 0;
491
492 /** Weight of proof method. */
493 private final int weight;
494
495 /** Order of proof method. */
496 private final int order;
497
498 SubstituteBase(final int weight, final int order) {
499 this.weight = weight;
500 this.order = order;
501 }
502
503 public int getWeight() {
504 return weight;
505 }
506
507 public int getOrder() {
508 return order;
509 }
510 public int nextLine() {
511 return next;
512 }
513
514 public int compareTo(final Object obj) {
515 if (obj instanceof Substitute) {
516 Substitute sub = (Substitute) obj;
517 // we don't return 0 because the TreeSet gets no more elements
518 // if we have methods with same order value
519 if (order == sub.getOrder()) {
520 return -1;
521 }
522 if (order < sub.getOrder()) {
523 return -1;
524 }
525 return 1;
526 }
527 return -1;
528 }
529
530 public void substitute() throws ProofException {
531 substitute(next);
532 next++;
533 }
534
535 public abstract void substitute(int i) throws ProofException;
536
537 }
538
539
540 /**
541 * Work on proof line and substitute proposition variables.
542 *
543 */
544 interface Substitute extends Comparable {
545
546 /**
547 * Return next proof line number we will work on.
548 *
549 * @return Next proof line number we will worked on.
550 */
551 public int nextLine();
552
553 /**
554 * Substitute next proof line number.
555 *
556 * @throws ProofException We found a proof or have to end the search!
557 */
558 public void substitute() throws ProofException;
559
560 /**
561 * Get weight of substitution rule. This is the number of runs for this
562 * substitution.
563 *
564 * @return Weight.
565 */
566 public int getWeight();
567
568 /**
569 * Get order position of substitution rule. This says about the sequence position of this
570 * substitution method.
571 *
572 * @return Order position.
573 */
574 public int getOrder();
575
576 }
577
578 }
|