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.list.Element;
21  import org.qedeq.kernel.se.base.module.Universal;
22  
23  
24  /**
25   * Usage of rule for universal generalization.
26   *
27   * Rule of universal generalization.
28   * <pre>
29   *   A -&gt; B(x)
30   *  -------------------
31   *   A -&gt; forall x  B(x)
32   * </pre>
33   *
34   * @author  Michael Meyling
35   */
36  public class UniversalVo implements Universal {
37  
38      /** Reference to previously proven formula. */
39      private String reference;
40  
41      /** Subject variable that we will quantify about. */
42      private Element subjectVariable;
43  
44      /**
45       * Constructs an reason.
46       *
47       * @param   reference                   Reference to a valid formula.
48       * @param   subjectVariable             Subject variable that we will quantify about.
49       */
50  
51      public UniversalVo(final String reference, final Element subjectVariable) {
52          this.reference = reference;
53          this.subjectVariable = subjectVariable;
54      }
55  
56      /**
57       * Default constructor.
58       */
59      public UniversalVo() {
60          // nothing to do
61      }
62  
63      public Universal getUniversal() {
64          return this;
65      }
66  
67      public String getReference() {
68          return reference;
69      }
70  
71      /**
72       * Set formula reference.
73       *
74       * @param   reference   Reference to formula.
75       */
76      public void setReference(final String reference) {
77          this.reference = reference;
78      }
79  
80      public String[] getReferences() {
81          if (reference == null) {
82              return ArrayUtils.EMPTY_STRING_ARRAY;
83          }
84          return new String[] {reference };
85      }
86  
87      public Element getSubjectVariable() {
88          return subjectVariable;
89      }
90  
91      /**
92       * Set quantification subject variable.
93       *
94       * @param   subjectVariable Set free subject variable.
95       */
96      public void setSubjectVariable(final Element subjectVariable) {
97          this.subjectVariable = subjectVariable;
98      }
99  
100     public String getName() {
101         return "Universal";
102     }
103 
104     public boolean equals(final Object obj) {
105         if (!(obj instanceof UniversalVo)) {
106             return false;
107         }
108         final UniversalVo other = (UniversalVo) obj;
109         return EqualsUtility.equals(reference, other.reference)
110             && EqualsUtility.equals(subjectVariable, other.subjectVariable);
111     }
112 
113     public int hashCode() {
114         return (reference != null ? reference.hashCode() : 0)
115             ^ (subjectVariable != null ? 2 ^ subjectVariable.hashCode() : 0);
116     }
117 
118     public String toString() {
119         StringBuffer result = new StringBuffer();
120         result.append(getName());
121         if (reference != null || subjectVariable != null) {
122             result.append(" (");
123             boolean w = false;
124             if (reference != null) {
125                 result.append(reference);
126                 w = true;
127             }
128             if (subjectVariable != null) {
129                 if (w) {
130                     result.append(", ");
131                 }
132                 result.append(subjectVariable);
133                 w = true;
134             }
135             result.append(")");
136         }
137         return result.toString();
138     }
139 
140 }