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.list.Element;
021 import org.qedeq.kernel.se.base.module.Universal;
022
023
024 /**
025 * Usage of rule for universal generalization.
026 *
027 * Rule of universal generalization.
028 * <pre>
029 * A -> B(x)
030 * -------------------
031 * A -> forall x B(x)
032 * </pre>
033 *
034 * @author Michael Meyling
035 */
036 public class UniversalVo implements Universal {
037
038 /** Reference to previously proven formula. */
039 private String reference;
040
041 /** Subject variable that we will quantify about. */
042 private Element subjectVariable;
043
044 /**
045 * Constructs an reason.
046 *
047 * @param reference Reference to a valid formula.
048 * @param subjectVariable Subject variable that we will quantify about.
049 */
050
051 public UniversalVo(final String reference, final Element subjectVariable) {
052 this.reference = reference;
053 this.subjectVariable = subjectVariable;
054 }
055
056 /**
057 * Default constructor.
058 */
059 public UniversalVo() {
060 // nothing to do
061 }
062
063 public Universal getUniversal() {
064 return this;
065 }
066
067 public String getReference() {
068 return reference;
069 }
070
071 /**
072 * Set formula reference.
073 *
074 * @param reference Reference to formula.
075 */
076 public void setReference(final String reference) {
077 this.reference = reference;
078 }
079
080 public String[] getReferences() {
081 if (reference == null) {
082 return ArrayUtils.EMPTY_STRING_ARRAY;
083 } else {
084 return new String[] {reference };
085 }
086 }
087
088 public Element getSubjectVariable() {
089 return subjectVariable;
090 }
091
092 /**
093 * Set quantification subject variable.
094 *
095 * @param subjectVariable Set free subject variable.
096 */
097 public void setSubjectVariable(final Element subjectVariable) {
098 this.subjectVariable = subjectVariable;
099 }
100
101 public String getName() {
102 return "Universal";
103 }
104
105 public boolean equals(final Object obj) {
106 if (!(obj instanceof UniversalVo)) {
107 return false;
108 }
109 final UniversalVo other = (UniversalVo) obj;
110 return EqualsUtility.equals(reference, other.reference)
111 && EqualsUtility.equals(subjectVariable, other.subjectVariable);
112 }
113
114 public int hashCode() {
115 return (reference != null ? reference.hashCode() : 0)
116 ^ (subjectVariable != null ? 2 ^ subjectVariable.hashCode() : 0);
117 }
118
119 public String toString() {
120 StringBuffer result = new StringBuffer();
121 result.append(getName());
122 if (reference != null || subjectVariable != null) {
123 result.append(" (");
124 boolean w = false;
125 if (reference != null) {
126 result.append(reference);
127 w = true;
128 }
129 if (subjectVariable != null) {
130 if (w) {
131 result.append(", ");
132 }
133 result.append(subjectVariable);
134 w = true;
135 }
136 result.append(")");
137 }
138 return result.toString();
139 }
140
141 }
|