com.articulate.sigma

Class 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()

Method Summary

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