com.articulate.sigma

Class Clausifier

java.lang.Object

com.articulate.sigma.Clausifier

public class Clausifier
extends java.lang.Object

The code in the section below implements an algorithm for translating SUO-KIF expressions to clausal form. The public methods are: public Formula clausify() public ArrayList clausifyWithRenameInfo() public ArrayList toNegAndPosLitsWithRenameInfo() The result is a single formula in conjunctive normal form (CNF), which is actually a set of (possibly negated) clauses surrounded by an "or".

Constructor Summary

Constructors

Constructor and Description
Clausifier(java.lang.String s)

Method Summary

Modifier and Type	Method and Description
Formula	clausify() This method converts the SUO-KIF Formula to a version of clausal (resolution, conjunctive normal) form with Skolem functions, following the procedure described in Logical Foundations of Artificial Intelligence, by Michael Genesereth and Nils Nilsson, 1987, pp.
static Formula	clausify(Formula f) convenience method
java.util.ArrayList	clausifyWithRenameInfo() Note this returns a List of mixed types! Fixme!
static java.util.Set<java.lang.String>	extractVariables(Formula f) Extract all variables in a list
static java.lang.String	getOriginalVar(java.lang.String var, java.util.Map<java.lang.String,java.lang.String> varMap) This method finds the original variable that corresponds to a new variable.
Formula	instantiateVariables() Create constants to fill variables.
static void	main(java.lang.String[] args)
protected static java.lang.String	normalizeVariables_1(java.lang.String input, int[] idxs, java.util.Map vmap, boolean replaceSkolemTerms) An internal helper method for normalizeVariables(String input).
static java.lang.String	normalizeVariables(java.lang.String input) Returns a String in which all variables and row variables have been normalized -- renamed, in depth-first order of occurrence, starting from index 1 -- to support comparison of Formulae for equality.
protected static java.lang.String	normalizeVariables(java.lang.String input, boolean replaceSkolemTerms) Returns a String in which all variables and row variables have been normalized -- renamed, in depth-first order of occurrence, starting from index 1 -- to support comparison of Formulae for equality.
Formula	rename(java.lang.String term2, java.lang.String term1) Replace term2 with term1
static Formula	renameVariables(Formula f) convenience method
static Formula	renameVariables(Formula f, java.util.Map topLevelVars, java.util.Map scopedRenames, java.util.Map allRenames) convenience method
java.util.ArrayList<Formula>	separateConjunctions() Turn a conjunction into an ArrayList of separate statements
static java.util.ArrayList<Formula>	separateConjunctions(Formula f) convenience method
Formula	substituteVariables(java.util.Map<java.lang.String,java.lang.String> m) Replace variables with a value as given by the map argument
static void	test1() A test method.
static void	testClausifier(java.lang.String[] args) A test method.
Formula	toCanonicalClausalForm() This method converts the SUO-KIF Formula to a canonical version of clausal (resolution, conjunctive normal) form with Skolem functions, following the procedure described in Logical Foundations of Artificial Intelligence, by Michael Genesereth and Nils Nilsson, 1987, pp.
static Formula	toCanonicalClausalForm(Formula f) convenience method
protected Formula	toCanonicalKifSpecialForm(boolean preserveSharedVariables) This method returns a canonical version of this Formula, assumed to be a KIF "special" form, in which all internal first-order KIF formulae are replaced by their canonical versions, and all variables are renamed, in left to right depth-first order of occurrence, starting from index 1.
java.util.ArrayList	toNegAndPosLitsWithRenameInfo() TODO: Note mixed types in return List! Fixme! This method converts the SUO-KIF Formula to an ArrayList of clauses.
static java.util.ArrayList	toNegAndPosLitsWithRenameInfo(Formula f) convenience method
protected Formula	toOpenQueryForNegatedDualForm() This method returns an open Formula that constitutes a KIF query expression, which is generated from the canonicalized negation of the original Formula.
java.lang.String	toString()
static Formula	universalsOut(Formula f) convenience method

Methods inherited from class java.lang.Object

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

Constructor Detail

Clausifier

public Clausifier(java.lang.String s)

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

separateConjunctions

public java.util.ArrayList<Formula> separateConjunctions()

Turn a conjunction into an ArrayList of separate statements

separateConjunctions

public static java.util.ArrayList<Formula> separateConjunctions(Formula f)

convenience method

clausify

public static Formula clausify(Formula f)

convenience method

clausifyWithRenameInfo

public java.util.ArrayList clausifyWithRenameInfo()

Note this returns a List of mixed types! Fixme!

Returns:

an ArrayList that contains three items: The new clausal-form Formula, the original (input) SUO-KIF Formula, and a Map containing a graph of all the variable substitions done during the conversion to clausal form. This Map makes it possible to retrieve the correspondence between the variables in the clausal form and the variables in the original Formula. Some elements might be null if a clausal form cannot be generated.

See Also:

clausify(), toNegAndPosLitsWithRenameInfo(), toCanonicalClausalForm();

toNegAndPosLitsWithRenameInfo

public java.util.ArrayList toNegAndPosLitsWithRenameInfo()

TODO: Note mixed types in return List! Fixme! This method converts the SUO-KIF Formula to an ArrayList of clauses. Each clause is an ArrayList containing an ArrayList of negative literals, and an ArrayList of positive literals. Either the neg lits list or the pos lits list could be empty. Each literal is a Formula object. The first object in the returned ArrayList is an ArrayList of clauses. The second object in the returned ArrayList is the original (input) Formula object (this). The third object in the returned ArrayList is a Map that contains a graph of all the variable substitions done during the conversion of this Formula to clausal form. This Map makes it possible to retrieve the correspondences between the variables in the clausal form and the variables in the original Formula.

Returns:

A three-element ArrayList, [ // 1. clauses [ // a clause [ // negative literals [ Formula1, Formula2, ..., FormulaN ], // positive literals [ Formula1, Formula2, ..., FormulaN ] ], // another clause [ // negative literals [ Formula1, Formula2, ..., FormulaN ], // positive literals [ Formula1, Formula2, ..., FormulaN ] ], ..., ], // 2. , // 3. {a-Map-of-variable-renamings}, ]

See Also:

clausify(), clausifyWithRenameInfo(), toCanonicalClausalForm();

toNegAndPosLitsWithRenameInfo

public static java.util.ArrayList toNegAndPosLitsWithRenameInfo(Formula f)

convenience method

toCanonicalClausalForm

public Formula toCanonicalClausalForm()

This method converts the SUO-KIF Formula to a canonical version of clausal (resolution, conjunctive normal) form with Skolem functions, following the procedure described in Logical Foundations of Artificial Intelligence, by Michael Genesereth and Nils Nilsson, 1987, pp. 63-66. In canonical form, all variables are renamed from index 0 and all literals are alphabetically sorted.

Returns:

The Formula in a canonicalized version of clausal form

See Also:

clausify(), clausifyWithRenameInfo(), toNegAndPosLitsWithRenameInfo()

toCanonicalClausalForm

public static Formula toCanonicalClausalForm(Formula f)

convenience method

toOpenQueryForNegatedDualForm

protected Formula toOpenQueryForNegatedDualForm()

This method returns an open Formula that constitutes a KIF query expression, which is generated from the canonicalized negation of the original Formula. The original Formula is assumed to be a "rule", having both positive and negative literals when converted to canonical clausal form. This method returns a query expression that can be used to test the validity of the original Formula. If the query succeeds (evaluates to true, or retrieves variable bindings), then the negation of the original Formula is valid, and the original Formula must be invalid.

Note that this method will work reliably only for standard first order KIF expressions, and probably will not produce expected (or sane) results if used with non-standard KIF.

Returns:

A String representing an open KIF query expression.

See Also:

Formula.toCanonicalClausalForm()

toCanonicalKifSpecialForm

protected Formula toCanonicalKifSpecialForm(boolean preserveSharedVariables)

This method returns a canonical version of this Formula, assumed to be a KIF "special" form, in which all internal first-order KIF formulae are replaced by their canonical versions, and all variables are renamed, in left to right depth-first order of occurrence, starting from index 1. This method is intended to be applied to higher-order constructs that expand the syntax of KIF. To canonicalize ordinary first-order KIF formulae, just use Formula.toCanonicalClausalForm().

Parameters:

preserveSharedVariables - If true, all variable sharing between embedded expressions will be preserved, even though all variables will still be renamed as part of the canonicalization process

Returns:

A String representing the canonicalized version of this special, non-standard KIF expression.

See Also:

Formula.toCanonicalClausalForm()

normalizeVariables

public static java.lang.String normalizeVariables(java.lang.String input)

Returns a String in which all variables and row variables have been normalized -- renamed, in depth-first order of occurrence, starting from index 1 -- to support comparison of Formulae for equality.

Parameters:

input - A String representing a SUO-KIF Formula, possibly containing variables to be normalized

Returns:

A String, typically representing a SUO-KIF Formula or part of a Formula, in which the original variables have been replaced by normalized forms

See Also:

normalizeVariables_1();

normalizeVariables

protected static java.lang.String normalizeVariables(java.lang.String input,
                                                     boolean replaceSkolemTerms)

Returns a String in which all variables and row variables have been normalized -- renamed, in depth-first order of occurrence, starting from index 1 -- to support comparison of Formulae for equality.

Parameters:

input - A String representing a SUO-KIF Formula, possibly containing variables to be normalized

replaceSkolemTerms - If true, all Skolem terms in input are treated as variables and are replaced with normalized variable terms

Returns:

A String, typically representing a SUO-KIF Formula or part of a Formula, in which the original variables have been replaced by normalized forms

See Also:

normalizeVariables_1();

normalizeVariables_1

protected static java.lang.String normalizeVariables_1(java.lang.String input,
                                                       int[] idxs,
                                                       java.util.Map vmap,
                                                       boolean replaceSkolemTerms)

An internal helper method for normalizeVariables(String input).

Parameters:

input - A String possibly containing variables to be normalized

idxs - A two-place int[] in which int[0] is the current variable index, and int[1] is the current row variable index

vmap - A Map in which the keys are old variables and the values are new variables

Returns:

A String, typically a representing a SUO-KIF Formula or part of a Formula.

See Also:

normalizeVariables();

rename

public Formula rename(java.lang.String term2,
                      java.lang.String term1)

Replace term2 with term1

substituteVariables

public Formula substituteVariables(java.util.Map<java.lang.String,java.lang.String> m)

Replace variables with a value as given by the map argument

extractVariables

public static java.util.Set<java.lang.String> extractVariables(Formula f)

Extract all variables in a list

instantiateVariables

public Formula instantiateVariables()

Create constants to fill variables.

renameVariables

public static Formula renameVariables(Formula f)

convenience method

renameVariables

public static Formula renameVariables(Formula f,
                                      java.util.Map topLevelVars,
                                      java.util.Map scopedRenames,
                                      java.util.Map allRenames)

convenience method

universalsOut

public static Formula universalsOut(Formula f)

convenience method

getOriginalVar

public static java.lang.String getOriginalVar(java.lang.String var,
                                              java.util.Map<java.lang.String,java.lang.String> varMap)

This method finds the original variable that corresponds to a new variable. Note that the clausification algorithm has two variable renaming steps, and that after variables are standardized apart an original variable might correspond to multiple clause variables.

Parameters:

var - A SUO-KIF variable (String)

varMap - A Map (graph) of successive new to old variable correspondences.

Returns:

The original SUO-KIF variable corresponding to the input.

clausify

public Formula clausify()

This method converts the SUO-KIF Formula to a version of clausal (resolution, conjunctive normal) form with Skolem functions, following the procedure described in Logical Foundations of Artificial Intelligence, by Michael Genesereth and Nils Nilsson, 1987, pp. 63-66.

A literal is an atomic formula. (Note, however, that because SUO-KIF allows higher-order formulae, not all SUO-KIF literals are really atomic.) A clause is a disjunction of literals that share no variable names with literals in any other clause in the KB. Note that even a relatively simple SUO-KIF formula might generate multiple clauses. In such cases, the Formula returned will be a conjunction of clauses. (A KB is understood to be a conjunction of clauses.) In all cases, the Formula returned by this method should be a well-formed SUO-KIF Formula if the input (original formula) is a well-formed SUO-KIF Formula. Rendering the output in true (LISPy) clausal form would require an additional step, the removal of all commutative logical operators, and the result would not be well-formed SUO-KIF.

Returns:

A SUO-KIF Formula in clausal form, or null if a clausal form cannot be generated.

See Also:

clausifyWithRenameInfo(), toNegAndPosLitsWithRenameInfo(), toCanonicalClausalForm();

test1

public static void test1()

A test method.

testClausifier

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

A test method.

main

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