001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, 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
022 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
023 import org.qedeq.kernel.bo.logic.common.Operators;
024 import org.qedeq.kernel.bo.logic.common.ProofFinder;
025 import org.qedeq.kernel.se.base.list.Element;
026 import org.qedeq.kernel.se.base.list.ElementList;
027 import org.qedeq.kernel.se.base.module.Add;
028 import org.qedeq.kernel.se.base.module.FormalProofLineList;
029 import org.qedeq.kernel.se.base.module.ModusPonens;
030 import org.qedeq.kernel.se.base.module.Reason;
031 import org.qedeq.kernel.se.common.ModuleContext;
032 import org.qedeq.kernel.se.dto.list.DefaultElementList;
033 import org.qedeq.kernel.se.dto.list.ElementSet;
034 import org.qedeq.kernel.se.visitor.InterruptException;
035
036
037 /**
038 * Find basic proofs for formulas.
039 *
040 * @author Michael Meyling
041 */
042 public class ProofFinderImpl implements ProofFinder {
043
044 /** List of proof lines. */
045 private List lines;
046
047 /** List of reasons. */
048 private List reasons;
049
050 /** Set of all predicate variables that occur in this proof anywhere. */
051 private ElementSet allPredVars;
052
053 /** Below this number MP was tried. */
054 private int mpLast;
055
056 /** Goal to prove. */
057 private Element goalFormula;
058
059 /**
060 * Constructor.
061 *
062 */
063 public ProofFinderImpl() {
064 }
065
066 public FormalProofLineList findProof(final Element formula,
067 final FormalProofLineList proof, final ModuleContext context) throws InterruptException {
068 this.goalFormula = formula;
069 lines = new ArrayList();
070 reasons = new ArrayList();
071 allPredVars = new ElementSet();
072 // add first proof formulas to our proof line list
073 for (int i = 0; i < proof.size(); i++) {
074 final Reason r = proof.get(i).getReasonType().getReason();
075 if (!(r instanceof Add)) {
076 continue;
077 }
078 lines.add(proof.get(i).getFormula().getElement());
079 reasons.add(r);
080 allPredVars.union(FormulaUtility.getPropositionVariables(
081 proof.get(i).getFormula().getElement()));
082 }
083 String max = "A";
084 final Iterator j = allPredVars.iterator();
085 while (j.hasNext()) {
086 final ElementList v = (ElementList) j.next();
087 final String name = v.getElement(0).getAtom().getString();
088 if (-1 == max.compareTo(name)) {
089 max = name;
090 }
091 }
092 max = (char) (max.charAt(0) + 1) + "";
093 System.out.println(max);
094 // add one extra predicate variable
095 allPredVars.add(FormulaUtility.createPredicateVariable(max));
096 for (int i = 0; i < lines.size(); i++) {
097 ProofFinderUtility.printUtf8Line(lines, reasons, i);
098 }
099 System.out.println("Goal: ");
100 ProofFinderUtility.println(formula);
101 int i = 0;
102 while (i < lines.size() && lines.size() < Integer.MAX_VALUE - 1000) {
103 try {
104 tryModusPonensAll();
105 if (Thread.interrupted()) {
106 throw new InterruptException(context);
107 }
108 trySubstitution(i++);
109 } catch (ProofFoundException e) {
110 System.out.println("proof found. lines: " + lines.size());
111 return ProofFinderUtility.shortenProof(lines, reasons);
112 }
113 }
114 System.out.println("proof not found. lines: " + lines.size());
115 return null;
116 }
117
118 private void tryModusPonensAll() throws ProofFoundException {
119 int until = lines.size();
120 for (int i = 0; i < until; i++) {
121 final Element first = (Element) lines.get(i);
122 if (!FormulaUtility.isImplication(first)) {
123 continue;
124 }
125 for (int j = (i < mpLast ? mpLast : 0); j < until; j++) {
126 if (first.getList().getElement(0).equals(
127 (Element) lines.get(j))) {
128 // System.out.println("MP found!");
129 final ModusPonens mp = new ModusPonensBo(i, j);
130 addFormula(first.getList().getElement(1), mp);
131 }
132 }
133 }
134 mpLast = until;
135 }
136
137 /**
138 * Make all possible substitutions in a proof line.
139 *
140 * @param i Proof line number we want to try substitution.
141 * @throws ProofFoundException We found a proof!
142 */
143 private void trySubstitution(final int i) throws ProofFoundException {
144 // System.out.print("subst " + i + " ");
145 final Element f = (Element) lines.get(i);
146 // FormulaUtility.println(f);
147 final ElementSet vars = FormulaUtility.getPredicateVariables(f);
148 // System.out.print("vars=");
149 // System.out.println(vars);
150 final Iterator iter = vars.iterator();
151 while (iter.hasNext()) {
152 final ElementList var = (ElementList) iter.next();
153 // System.out.print("var=");
154 // FormulaUtility.println(var);
155 // substitute by different variable
156 {
157 // System.out.print("allPredVars=");
158 // System.out.println(allPredVars);
159 final Iterator all = allPredVars.iterator();
160 while (all.hasNext()) {
161 final ElementList subst = (ElementList) all.next();
162 if (var.equals(subst)) {
163 continue;
164 }
165 final Element created = FormulaUtility.replaceOperatorVariable(
166 f, var, subst);
167 addFormula(created, new SubstPredBo(i, var, subst));
168 }
169 }
170 // // substitute by negation
171 // {
172 // final Iterator all = allPredVars.iterator();
173 // while (all.hasNext()) {
174 // final ElementList var2 = (ElementList) all.next();
175 // final ElementList subst = new DefaultElementList(Operators.NEGATION_OPERATOR);
176 // subst.add(var2);
177 // final Element created = FormulaUtility.replaceOperatorVariable(
178 // f, var, subst);
179 // addFormula(created, new SubstPredBo(i, var, subst));
180 // }
181 // }
182 // // substitute by conjunction with another variable
183 // createReplacement(i, f, var, Operators.CONJUNCTION_OPERATOR, true);
184 // createReplacement(i, f, var, Operators.CONJUNCTION_OPERATOR, false);
185 // substitute by disjunction with another variable
186 createReplacement(i, f, var, Operators.DISJUNCTION_OPERATOR, true);
187 createReplacement(i, f, var, Operators.DISJUNCTION_OPERATOR, false);
188 // // substitute by implication with another variable
189 // createReplacement(i, f, var, Operators.EQUIVALENCE_OPERATOR, true);
190 // createReplacement(i, f, var, Operators.EQUIVALENCE_OPERATOR, false);
191 }
192 }
193
194 /**
195 * Substitute predicate variable <code>var</code> by binary operator with old variable
196 * and new variable and add this as a new proof line.
197 *
198 * @param i Proof line number we work on.
199 * @param f Proof line formula.
200 * @param var Predicate variable we want to replace.
201 * @param operator Operator of replacement formula.
202 * @param left Is old variable at left hand of new operator?
203 * @throws ProofFoundException We found a proof!
204 */
205 private void createReplacement(final int i, final Element f,
206 final ElementList var, final String operator, final boolean left) throws ProofFoundException {
207 final Iterator a = allPredVars.iterator();
208 while (a.hasNext()) {
209 final ElementList var2 = (ElementList) a.next();
210 final ElementList subst = new DefaultElementList(operator);
211 if (left) {
212 subst.add(var);
213 subst.add(var2);
214 } else {
215 subst.add(var2);
216 subst.add(var);
217 }
218 final Element created = FormulaUtility.replaceOperatorVariable(
219 f, var, subst);
220 addFormula(created, new SubstPredBo(i, var, subst));
221 }
222 }
223
224 private void addFormula(final Element formula, final Reason reason) throws ProofFoundException {
225 if (!lines.contains(formula)) {
226 lines.add(formula);
227 reasons.add(reason);
228 // printLine(lines.size() - 1);
229 if (goalFormula.equals(formula)) {
230 throw new ProofFoundException();
231 }
232 if ((lines.size() - 1) % 1000 == 0) {
233 ProofFinderUtility.printUtf8Line(lines, reasons, lines.size() - 1);
234 }
235 }
236 }
237
238 public String getExecutionActionDescription() {
239 return ProofFinderUtility.getUtf8Line(lines, reasons, lines.size() - 1);
240 }
241
242
243 /**
244 * Indicates we fond a proof.
245 *
246 * @author Michael Meyling.
247 *
248 */
249 private static class ProofFoundException extends Exception {
250
251 }
252
253 }
|