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 Summary

Fields

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

Constructor Summary

Constructors

Constructor and Description
ProofStep()

Method Summary

Modifier and Type	Method and Description
static ArrayList<ProofStep>	normalizeProofStepNumbers(ArrayList<ProofStep> proofSteps) Take an ArrayList of ProofSteps and renumber them consecutively starting at 1.
static ArrayList<ProofStep>	removeDuplicates(ArrayList<ProofStep> proofSteps) Take an ArrayList of ProofSteps and renumber them consecutively starting at 1.
static ArrayList<ProofStep>	removeUnnecessary(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;
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 String QUERY

See Also:

Constant Field Values

NEGATED_QUERY

public static final String NEGATED_QUERY

See Also:

Constant Field Values

INSTANTIATED_QUERY

public static final String INSTANTIATED_QUERY

See Also:

Constant Field Values

formulaType

public String formulaType

A String of the type clause or formula

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 KIF expression, that is the axiom expressing the conclusion of this proof step.

number

public Integer number

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

premises

public ArrayList<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 ArrayList<ProofStep> normalizeProofStepNumbers(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 ArrayList<ProofStep> removeDuplicates(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 ArrayList<ProofStep> removeUnnecessary(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 String toString()

Overrides:

toString in class Object