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.base.module;
17  
18  import org.qedeq.kernel.se.base.list.Element;
19  
20  
21  /**
22   * Rule of universal generalization.
23   * <pre>
24   *   A -&gt; B(x)
25   *  -------------------
26   *   A -&gt; forall x  B(x)
27   * </pre>
28   *
29   * @author  Michael Meyling
30   */
31  public interface Universal extends Reason {
32  
33      /**
34       * Get this reason.
35       *
36       * @return  This reason.
37       */
38      public Universal getUniversal();
39      /**
40       * Get reference to formula. Usually this a formula of type A -&gt; B(x)
41       *
42       * @return  Reference to previously proved formula.
43       */
44      public String getReference();
45  
46      /**
47       * Get free subject variable we want to quantify over.
48       *
49       * @return  Free subject variable.
50       */
51      public Element getSubjectVariable();
52  
53  }