org.jscience.linguistics.kif
Class Formula

java.lang.Object
  extended by 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.