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