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  
19  /**
20   * Usage of Modus Ponens.
21   * <pre>
22   *  A -&gt; B
23   *    A
24   *  ------
25   *    B
26   * </pre>
27   *
28   * @author  Michael Meyling
29   */
30  public interface ModusPonens extends Reason {
31  
32      /**
33       * Get this reason.
34       *
35       * @return  This reason.
36       */
37      public ModusPonens getModusPonens();
38  
39      /**
40       * Get reference to formula. Usually this a formula of type A -&gt; B
41       *
42       * @return  Reference to previously proved formula.
43       */
44      public String getReference1();
45  
46      /**
47       * Get reference to formula. Usually this a formula of type A
48       *
49       * @return  Reference to previously proved formula.
50       */
51      public String getReference2();
52  
53  }