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