View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2    *
3    * Copyright 2000-2014,  Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
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.se.dto.module;
17  
18  import org.apache.commons.lang.ArrayUtils;
19  import org.qedeq.base.utility.EqualsUtility;
20  import org.qedeq.kernel.se.base.module.Conclusion;
21  import org.qedeq.kernel.se.base.module.ConditionalProof;
22  import org.qedeq.kernel.se.base.module.FormalProofLineList;
23  import org.qedeq.kernel.se.base.module.Formula;
24  import org.qedeq.kernel.se.base.module.Hypothesis;
25  import org.qedeq.kernel.se.base.module.Reason;
26  
27  
28  /**
29   * Usage of conditional proof method. If you can derive the proposition A out of
30   * the assumed formulas then the following formula is true:
31   * conjunction of the assumed formulas implies A.
32   *
33   * @author  Michael Meyling
34   */
35  public class ConditionalProofVo implements ConditionalProof {
36  
37      /** Hypothesis. */
38      private Hypothesis hypothesis;
39  
40      /** Proof lines term. */
41      private FormalProofLineList formalProofLineList;
42  
43      /** Conclusion. */
44      private Conclusion conclusion;
45  
46      /**
47       * Constructs an reason.
48       *
49       * @param   hypothesis              Free subject variable that will be replaced.
50       * @param   proofLines              Bound subject variable that will be substituted.
51       * @param   conclusion              Conclusion.
52       */
53      public ConditionalProofVo(final Hypothesis hypothesis, final FormalProofLineList proofLines,
54              final Conclusion conclusion) {
55          this.hypothesis = hypothesis;
56          this.formalProofLineList = proofLines;
57          this.conclusion = conclusion;
58      }
59  
60      /**
61       * Default constructor.
62       */
63      public ConditionalProofVo() {
64          // nothing to do
65      }
66  
67      public ConditionalProof getConditionalProof() {
68          return this;
69      }
70  
71      public Hypothesis getHypothesis() {
72          return hypothesis;
73      }
74  
75      /**
76       * Set hypothesis.
77       *
78       * @param   hypothesis  Reference to formula.
79       */
80      public void setHypothesis(final Hypothesis hypothesis) {
81          this.hypothesis = hypothesis;
82      }
83  
84      public String[] getReferences() {
85          return ArrayUtils.EMPTY_STRING_ARRAY;
86      }
87  
88      /**
89       * Set formal proof lines.
90       *
91       * @param   list    Proof lines that might use hypothesis.
92       */
93      public void setFormalProofLineList(final FormalProofLineList list) {
94          this.formalProofLineList = list;
95      }
96  
97      public FormalProofLineList getFormalProofLineList() {
98          return formalProofLineList;
99      }
100 
101     public Conclusion getConclusion() {
102         return conclusion;
103     }
104 
105     /**
106      * Set conclusion.
107      *
108      * @param   conclusion  New derived formula.
109      */
110     public void setConclusion(final Conclusion conclusion) {
111         this.conclusion = conclusion;
112     }
113 
114     public Formula getFormula() {
115         if (conclusion == null)  {
116             return null;
117         }
118         return conclusion.getFormula();
119     }
120 
121     public String getLabel() {
122         if (conclusion == null)  {
123             return null;
124         }
125         return conclusion.getLabel();
126     }
127 
128     public String getName() {
129         return "CP";
130     }
131 
132     public Reason getReason() {
133         return this;
134     }
135 
136     public boolean equals(final Object obj) {
137         if (!(obj instanceof ConditionalProofVo)) {
138             return false;
139         }
140         final ConditionalProofVo other = (ConditionalProofVo) obj;
141         return EqualsUtility.equals(hypothesis, other.hypothesis)
142             && EqualsUtility.equals(formalProofLineList, other.formalProofLineList)
143             && EqualsUtility.equals(conclusion, other.conclusion);
144     }
145 
146     public int hashCode() {
147         return (hypothesis != null ? hypothesis.hashCode() : 0)
148             ^ (formalProofLineList != null ? 2 ^ formalProofLineList.hashCode() : 0)
149             ^ (conclusion != null ? 4 ^ conclusion.hashCode() : 0);
150     }
151 
152     public String toString() {
153         StringBuffer result = new StringBuffer();
154         result.append(getName());
155         if (hypothesis != null || formalProofLineList != null || conclusion != null) {
156             result.append(" (");
157             if (hypothesis != null) {
158                 result.append("\n");
159                 result.append(hypothesis);
160             }
161             if (formalProofLineList != null) {
162                 result.append("\n");
163                 result.append(formalProofLineList);
164             }
165             if (conclusion != null) {
166                 result.append("\n");
167                 result.append(conclusion);
168             }
169             result.append("\n");
170             result.append(")");
171         }
172         return result.toString();
173     }
174 
175 }