org.jscience.linguistics.kif
Class Formula

java.lang.Object
  org.jscience.linguistics.kif.Formula

All Implemented Interfaces:

java.lang.Comparable

public class Formula
extends java.lang.Object
implements java.lang.Comparable

Handle operations on an individual formula. This includes formatting for presentation as well as pre-processing for sending to the inference engine.

Field Summary

int	endLine The line in the file on which the formula ends.
java.lang.String	sourceFile The source file in which the formula appears.
int	startLine The line in the file on which the formula starts.
java.lang.String	theFormula The formula.

Constructor Summary

Formula()

Method Summary

java.util.ArrayList	argumentsToArrayList(int start) ************************************************************** Return all the arguments in a simple formula as a list, starting at the given argument.
java.lang.String	car() ************************************************************** Return the LISP 'car' of the formula - the first element of the list.
java.lang.String	cdr() ************************************************************** Return the LISP 'cdr' of the formula - the rest of a list minus its first element.
int	compareTo(java.lang.Object f) ************************************************************** Implement the Comparable interface by defining the compareTo method.
boolean	deepEquals(Formula f) ************************************************************** Test if the contents of the formula are equal to the argument.
boolean	equals(java.lang.String s) ************************************************************** Test if the contents of the formula are equal to the String argument.
java.lang.String	format(java.lang.String hyperlink, java.lang.String indentChars, java.lang.String eolChars) ************************************************************** Format a formula for either text or HTML presentation by inserting the proper hyperlink code, characters for indentation and end of line.
java.lang.String	getArgument(int argnum) ************************************************************** Return the numbered argument of the given formula.
java.lang.String	htmlFormat(java.lang.String html) ************************************************************** Format a formula for HTML presentation.
static boolean	isNegatedQuery(java.lang.String query, java.lang.String formula) ************************************************************** Compare the given formula to the negated query and return whether they are the same (minus the negation).
boolean	logicallyEquals(java.lang.String s) ************************************************************** Test if the contents of the formula are equal to the argument at a deeper level than a simple string equals.
static void	main(java.lang.String[] args) ************************************************************** A test method.
java.lang.String	makeQuantifiersExplicit() ************************************************************** Makes implicit universal quantification explicit.
static java.lang.String	postProcess(java.lang.String s) ************************************************************** Remove the 'holds' prefix wherever it appears.
java.util.ArrayList	preProcess() ************************************************************** Pre-process a formula before sending it to Vampire.
void	read(java.lang.String s) ************************************************************** Read a String into the variable 'theFormula'.
java.lang.String	textFormat() Deprecated.
java.lang.String	toString() ************************************************************** Format a formula for text presentation.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

sourceFile

public java.lang.String sourceFile

The source file in which the formula appears.

startLine

public int startLine

The line in the file on which the formula starts.

endLine

public int endLine

The line in the file on which the formula ends.

theFormula

public java.lang.String theFormula

The formula.

Constructor Detail

Formula

public Formula()

Method Detail

read

public void read(java.lang.String s)

************************************************************** Read a String into the variable 'theFormula'.

compareTo

public int compareTo(java.lang.Object f)
              throws java.lang.ClassCastException

************************************************************** Implement the Comparable interface by defining the compareTo method. Formulas are equal if their formula strings are equal.

Specified by:

compareTo in interface java.lang.Comparable

Throws:

java.lang.ClassCastException

car

public java.lang.String car()

************************************************************** Return the LISP 'car' of the formula - the first element of the list. Note that this operation has no side effect on the Formula.

cdr

public java.lang.String cdr()

************************************************************** Return the LISP 'cdr' of the formula - the rest of a list minus its first element. Note that this operation has no side effect on the Formula.

logicallyEquals

public boolean logicallyEquals(java.lang.String s)

************************************************************** Test if the contents of the formula are equal to the argument at a deeper level than a simple string equals. The only logical manipulation is to treat conjunctions and disjunctions as unordered bags of clauses. So (and A B C) will be logicallyEqual(s) for example, to (and B A C). Note that this is a fairly time-consuming operation and should not generally be used for comparing large sets of formulas.

equals

public boolean equals(java.lang.String s)

************************************************************** Test if the contents of the formula are equal to the String argument. Normalize all variables.

deepEquals

public boolean deepEquals(Formula f)

************************************************************** Test if the contents of the formula are equal to the argument.

getArgument

public java.lang.String getArgument(int argnum)

************************************************************** Return the numbered argument of the given formula. The first element of a formula (i.e. the predicate position) is number 0. Returns the empty string if there is no such argument position.

argumentsToArrayList

public java.util.ArrayList argumentsToArrayList(int start)

************************************************************** Return all the arguments in a simple formula as a list, starting at the given argument. If formula is complex (i.e. an argument is a function or sentence), then return null. If the starting argument is greater than the number of arguments, also return null.

makeQuantifiersExplicit

public java.lang.String makeQuantifiersExplicit()

************************************************************** Makes implicit universal quantification explicit. May be needed in the future for other theorem provers.

preProcess

public java.util.ArrayList preProcess()

************************************************************** Pre-process a formula before sending it to Vampire. This includes ignoring meta-knowledge like documentation strings, translating mathematical operators, quoting higher-order formulas, expanding row variables and prepending the 'holds' predicate.

Returns:

an ArrayList of Formula(s)

isNegatedQuery

public static boolean isNegatedQuery(java.lang.String query,
                                     java.lang.String formula)

************************************************************** Compare the given formula to the negated query and return whether they are the same (minus the negation).

postProcess

public static java.lang.String postProcess(java.lang.String s)

************************************************************** Remove the 'holds' prefix wherever it appears.

format

public java.lang.String format(java.lang.String hyperlink,
                               java.lang.String indentChars,
                               java.lang.String eolChars)

************************************************************** Format a formula for either text or HTML presentation by inserting the proper hyperlink code, characters for indentation and end of line. A standard LISP-style pretty printing is employed where an open parenthesis triggers a new line and added indentation.

Parameters:

hyperlink - - the URL to be referenced to a hyperlinked term.

indentChars - - the proper characters for indenting text.

eolChars - - the proper character for end of line.

textFormat

public java.lang.String textFormat()

Deprecated.

************************************************************** Format a formula for text presentation.

toString

public java.lang.String toString()

************************************************************** Format a formula for text presentation.

Overrides:

toString in class java.lang.Object

htmlFormat

public java.lang.String htmlFormat(java.lang.String html)

************************************************************** Format a formula for HTML presentation.

main

public static void main(java.lang.String[] args)

************************************************************** A test method.