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.se.dto.module;
017
018 import org.qedeq.base.utility.EqualsUtility;
019 import org.qedeq.kernel.se.base.module.Conclusion;
020 import org.qedeq.kernel.se.base.module.ConditionalProof;
021 import org.qedeq.kernel.se.base.module.FormalProofLineList;
022 import org.qedeq.kernel.se.base.module.Formula;
023 import org.qedeq.kernel.se.base.module.Hypothesis;
024 import org.qedeq.kernel.se.base.module.Reason;
025
026
027 /**
028 * Usage of conditional proof method. If you can derive the proposition A out of
029 * the assumed formulas then the following formula is true:
030 * conjunction of the assumed formulas implies A.
031 *
032 * @author Michael Meyling
033 */
034 public class ConditionalProofVo implements ConditionalProof {
035
036 /** Hypothesis. */
037 private Hypothesis hypothesis;
038
039 /** Proof lines term. */
040 private FormalProofLineList proofLines;
041
042 /** Conclusion. */
043 private Conclusion conclusion;
044
045 /**
046 * Constructs an reason.
047 *
048 * @param hypothesis Free subject variable that will be replaced.
049 * @param proofLines Bound subject variable that will be substituted.
050 * @param conclusion Conclusion.
051 */
052 public ConditionalProofVo(final Hypothesis hypothesis, final FormalProofLineList proofLines,
053 final Conclusion conclusion) {
054 this.hypothesis = hypothesis;
055 this.proofLines = proofLines;
056 this.conclusion = conclusion;
057 }
058
059 /**
060 * Default constructor.
061 */
062 public ConditionalProofVo() {
063 // nothing to do
064 }
065
066 public ConditionalProof getConditionalProof() {
067 return this;
068 }
069
070 public Hypothesis getHypothesis() {
071 return hypothesis;
072 }
073
074 /**
075 * Set hypothesis.
076 *
077 * @param hypothesis Reference to formula.
078 */
079 public void setHypothesis(final Hypothesis hypothesis) {
080 this.hypothesis = hypothesis;
081 }
082
083 public String[] getReferences() {
084 return new String[0];
085 }
086
087 /**
088 * Set proof.
089 *
090 * @param list Proof.
091 */
092 public void setFormalProofLineList(final FormalProofLineList list) {
093 this.proofLines = list;
094 }
095
096 public FormalProofLineList getFormalProofLineList() {
097 return proofLines;
098 }
099
100 /**
101 * Set formal proof lines.
102 *
103 * @param proofLines Proof lines that might use hypothesis.
104 */
105 public void setFormalProofLinesList(final FormalProofLineList proofLines) {
106 this.proofLines = proofLines;
107 }
108
109 public Conclusion getConclusion() {
110 return conclusion;
111 }
112
113 /**
114 * Set conclusion.
115 *
116 * @param conclusion New derived formula.
117 */
118 public void setConclusion(final Conclusion conclusion) {
119 this.conclusion = conclusion;
120 }
121
122 public Formula getFormula() {
123 if (conclusion == null) {
124 return null;
125 }
126 return conclusion.getFormula();
127 }
128
129 public String getLabel() {
130 if (conclusion == null) {
131 return null;
132 }
133 return conclusion.getLabel();
134 }
135
136 public String getName() {
137 return "CP";
138 }
139
140 public Reason getReason() {
141 return this;
142 }
143
144 public boolean equals(final Object obj) {
145 if (!(obj instanceof ConditionalProofVo)) {
146 return false;
147 }
148 final ConditionalProofVo other = (ConditionalProofVo) obj;
149 return EqualsUtility.equals(hypothesis, other.hypothesis)
150 && EqualsUtility.equals(proofLines, other.proofLines)
151 && EqualsUtility.equals(conclusion, other.conclusion);
152 }
153
154 public int hashCode() {
155 return (hypothesis != null ? hypothesis.hashCode() : 0)
156 ^ (proofLines != null ? 2 ^ proofLines.hashCode() : 0)
157 ^ (conclusion != null ? 4 ^ conclusion.hashCode() : 0);
158 }
159
160 public String toString() {
161 StringBuffer result = new StringBuffer();
162 result.append(getName());
163 if (hypothesis != null || proofLines != null) {
164 result.append(" (");
165 if (hypothesis != null) {
166 result.append("\n");
167 result.append(hypothesis);
168 }
169 if (proofLines != null) {
170 result.append("\n");
171 result.append(proofLines);
172 }
173 if (conclusion != null) {
174 result.append("\n");
175 result.append(conclusion);
176 }
177 result.append("\n");
178 result.append(")");
179 }
180 return result.toString();
181 }
182
183 }
|