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.se.dto.module;
017
018 import org.apache.commons.lang.ArrayUtils;
019 import org.qedeq.base.utility.EqualsUtility;
020 import org.qedeq.kernel.se.base.module.Conclusion;
021 import org.qedeq.kernel.se.base.module.ConditionalProof;
022 import org.qedeq.kernel.se.base.module.FormalProofLineList;
023 import org.qedeq.kernel.se.base.module.Formula;
024 import org.qedeq.kernel.se.base.module.Hypothesis;
025 import org.qedeq.kernel.se.base.module.Reason;
026
027
028 /**
029 * Usage of conditional proof method. If you can derive the proposition A out of
030 * the assumed formulas then the following formula is true:
031 * conjunction of the assumed formulas implies A.
032 *
033 * @author Michael Meyling
034 */
035 public class ConditionalProofVo implements ConditionalProof {
036
037 /** Hypothesis. */
038 private Hypothesis hypothesis;
039
040 /** Proof lines term. */
041 private FormalProofLineList formalProofLineList;
042
043 /** Conclusion. */
044 private Conclusion conclusion;
045
046 /**
047 * Constructs an reason.
048 *
049 * @param hypothesis Free subject variable that will be replaced.
050 * @param proofLines Bound subject variable that will be substituted.
051 * @param conclusion Conclusion.
052 */
053 public ConditionalProofVo(final Hypothesis hypothesis, final FormalProofLineList proofLines,
054 final Conclusion conclusion) {
055 this.hypothesis = hypothesis;
056 this.formalProofLineList = proofLines;
057 this.conclusion = conclusion;
058 }
059
060 /**
061 * Default constructor.
062 */
063 public ConditionalProofVo() {
064 // nothing to do
065 }
066
067 public ConditionalProof getConditionalProof() {
068 return this;
069 }
070
071 public Hypothesis getHypothesis() {
072 return hypothesis;
073 }
074
075 /**
076 * Set hypothesis.
077 *
078 * @param hypothesis Reference to formula.
079 */
080 public void setHypothesis(final Hypothesis hypothesis) {
081 this.hypothesis = hypothesis;
082 }
083
084 public String[] getReferences() {
085 return ArrayUtils.EMPTY_STRING_ARRAY;
086 }
087
088 /**
089 * Set formal proof lines.
090 *
091 * @param list Proof lines that might use hypothesis.
092 */
093 public void setFormalProofLineList(final FormalProofLineList list) {
094 this.formalProofLineList = list;
095 }
096
097 public FormalProofLineList getFormalProofLineList() {
098 return formalProofLineList;
099 }
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 }
|