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.service.logic;
17
18 import org.qedeq.base.io.Parameters;
19 import org.qedeq.kernel.bo.module.KernelQedeqBo;
20 import org.qedeq.kernel.bo.module.PluginBo;
21 import org.qedeq.kernel.bo.module.PluginExecutor;
22
23
24 /**
25 * Finds primitive formal proofs.
26 *
27 * @author Michael Meyling
28 */
29 public final class SimpleProofFinderPlugin implements PluginBo {
30
31 /** This class. */
32 private static final Class CLASS = SimpleProofFinderPlugin.class;
33
34 public String getPluginId() {
35 return CLASS.getName();
36 }
37
38 public String getPluginActionName() {
39 return "Find Proofs";
40 }
41
42 public String getPluginDescription() {
43 return "finds simple formal proofs and add them to module [EXPERIMENTAL]";
44 }
45
46 public PluginExecutor createExecutor(final KernelQedeqBo qedeq, final Parameters parameters) {
47 return new SimpleProofFinderExecutor(this, qedeq, parameters);
48 }
49
50 public void setDefaultValuesForEmptyPluginParameters(final Parameters parameters) {
51 parameters.setDefault("extraVars", 1);
52 parameters.setDefault("maximumProofLines", Integer.MAX_VALUE - 2);
53 parameters.setDefault("skipFormulas", "");
54 parameters.setDefault("propositionVariableWeight", 3);
55 parameters.setDefault("propositionVariableOrder", 1);
56 parameters.setDefault("partFormulaOrder", 2);
57 parameters.setDefault("partFormulaWeight", 1);
58 parameters.setDefault("disjunctionOrder", 3);
59 parameters.setDefault("disjunctionWeight", 3);
60 parameters.setDefault("implicationOrder", 4);
61 parameters.setDefault("implicationWeight", 1);
62 parameters.setDefault("negationOrder", 5);
63 parameters.setDefault("negationWeight", 1);
64 parameters.setDefault("conjunctionOrder", 6);
65 parameters.setDefault("conjunctionWeight", 1);
66 parameters.setDefault("equivalenceOrder", 7);
67 parameters.setDefault("equivalenceWeight", 1);
68 parameters.setDefault("logFrequence", 1000);
69 parameters.setDefault("noSave", false);
70 }
71
72 }
|