ProofStep

java.lang.Object
- com.articulate.sigma.ProofStep

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

Field Summary

Fields
Modifier and Type	Field and Description
`java.lang.String`	`axiom` A String containing a valid KIF expression, that is the axiom expressing the conclusion of this proof step.
`java.lang.String`	`formulaRole` A String of the role of the formula
`java.lang.String`	`formulaType` A String of the type clause or formula
`java.lang.String`	`inferenceType` A String of the inference type, e.g.
`static java.lang.String`	`INSTANTIATED_QUERY`
`static java.lang.String`	`NEGATED_QUERY`
`java.lang.Integer`	`number` The number assigned to this proof step, initially by EProver and then normalized by ProofStep.normalizeProofStepNumbers()
`java.util.ArrayList<java.lang.Integer>`	`premises` An ArrayList of Integer(s), which reference prior proof steps from which this axiom is derived.
`static java.lang.String`	`QUERY`

Constructor Summary

Constructors
Constructor and Description

ProofStep()

Constructors
Constructor and Description
`ProofStep()`

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`static java.util.ArrayList<ProofStep>`	`normalizeProofStepNumbers(java.util.ArrayList<ProofStep> proofSteps)` Take an ArrayList of ProofSteps and renumber them consecutively starting at 1.
`static java.util.ArrayList<ProofStep>`	`removeDuplicates(java.util.ArrayList<ProofStep> proofSteps)` Take an ArrayList of ProofSteps and renumber them consecutively starting at 1.
`static java.util.ArrayList<ProofStep>`	`removeUnnecessary(java.util.ArrayList<ProofStep> proofSteps)` created a new by qingqing remove unnecessary steps, which should not appear in proof Unnecessary steps could be: (1) conjectures; (2) Successful resolution theorem proving results in a contradiction;
`java.lang.String`	`toString()`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - QUERY
```
public static final java.lang.String QUERY
```
    See Also:
    
    Constant Field Values
  - NEGATED_QUERY
```
public static final java.lang.String NEGATED_QUERY
```
    See Also:
    
    Constant Field Values
  - INSTANTIATED_QUERY
```
public static final java.lang.String INSTANTIATED_QUERY
```
    See Also:
    
    Constant Field Values
  - formulaType
```
public java.lang.String formulaType
```
    A String of the type clause or formula
  - formulaRole
```
public java.lang.String formulaRole
```
    A String of the role of the formula
  - inferenceType
```
public java.lang.String inferenceType
```
    A String of the inference type, e.g. add_answer_literal | assume_negation | etc.
  - axiom
```
public java.lang.String axiom
```
    A String containing a valid KIF expression, that is the axiom expressing the conclusion of this proof step.
  - number
```
public java.lang.Integer number
```
    The number assigned to this proof step, initially by EProver and then normalized by ProofStep.normalizeProofStepNumbers()
  - premises
```
public java.util.ArrayList<java.lang.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 Detail
  - ProofStep
```
public ProofStep()
```
- Method Detail
  - normalizeProofStepNumbers
```
public static java.util.ArrayList<ProofStep> normalizeProofStepNumbers(java.util.ArrayList<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 java.util.ArrayList<ProofStep> removeDuplicates(java.util.ArrayList<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.
  - removeUnnecessary
```
public static java.util.ArrayList<ProofStep> removeUnnecessary(java.util.ArrayList<ProofStep> proofSteps)
```
    created a new by qingqing remove unnecessary steps, which should not appear in proof Unnecessary steps could be: (1) conjectures; (2) Successful resolution theorem proving results in a contradiction;
  - toString
```
public java.lang.String toString()
```
    Overrides:
    
    toString in class java.lang.Object

Class ProofStep

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

QUERY

NEGATED_QUERY

INSTANTIATED_QUERY

formulaType

formulaRole

inferenceType

axiom

number

premises

Constructor Detail

ProofStep

Method Detail

normalizeProofStepNumbers

removeDuplicates

removeUnnecessary

toString