Package com.articulate.sigma

Class ProofStep

java.lang.Object
com.articulate.sigma.ProofStep
public class ProofStep extends Object
A trivial structure to hold the elements of a proof step.

  • Field Details

    • debug

      public static boolean debug

    • QUERY

      public static final String QUERY
      See Also:

    • NEGATED_QUERY

      public static final String NEGATED_QUERY
      See Also:

    • INSTANTIATED_QUERY

      public static final String INSTANTIATED_QUERY
      See Also:

    • input

      public String input

    • formulaType

      public String formulaType
      A String giving the type of the clause or formula, such as 'conjecture', 'plain' or 'axiom'

    • formulaRole

      public String formulaRole
      A String of the role of the formula

    • inferenceType

      public String inferenceType
      A String of the inference type, e.g. add_answer_literal | assume_negation | etc.

    • axiom

      public String axiom
      A String containing a valid SUO-KIF expression, that is the axiom expressing the conclusion of this proof step.

    • sourceID

      public String sourceID

    • number

      public Integer number
      The number assigned to this proof step, initially by EProver and then normalized by ProofStep.normalizeProofStepNumbers()

    • premises

      public List<Integer> premises
      An ArrayList of Integer(s), which reference prior proof steps from which this axiom is derived. Note that the numbering is what the ProofProcessor assigns, not necessarily the proof numbers returned directly from the inference engine.

  • Constructor Details

    • ProofStep

      public ProofStep()

  • Method Details

    • normalizeProofStepNumbers

      public static List<ProofStep> normalizeProofStepNumbers(List<ProofStep> proofSteps)
      Take an ArrayList of ProofSteps and renumber them consecutively starting at 1. Update the ArrayList of premises so that they reflect the renumbering.

    • removeDuplicates

      public static List<ProofStep> removeDuplicates(List<ProofStep> proofSteps)
      Remove duplicate statements in the proof

    • removeUnnecessary

      public static List<ProofStep> removeUnnecessary(List<ProofStep> proofSteps)
      created by qingqing remove unnecessary steps, which should not appear in proof Unnecessary steps could be: (1) conjecture (2) duplicate $false;

    • toString

      public String toString()
      Overrides:
      toString in class Object