Package com.articulate.sigma

Class Clausifier

java.lang.Object
com.articulate.sigma.Clausifier
public class Clausifier extends 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".

  • Field Details

    • resetSkolem

      public static boolean resetSkolem

  • Constructor Details

    • Clausifier

      public Clausifier(String s)

  • Method Details

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • separateConjunctions

      public List<Formula> separateConjunctions()
      Turn a conjunction into an ArrayList of separate statements

    • separateConjunctions

      public static List<Formula> separateConjunctions(Formula f)
      convenience method

    • clausify

      public static Formula clausify(Formula f)
      convenience method

    • clausifyWithRenameInfo

      public List 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 substitutions 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:

    • toNegAndPosLitsWithRenameInfo

      public List 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 substitutions 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. invalid input: '<'the-original-Formula>, // 3. {a-Map-of-variable-renamings}, ]
      See Also:

    • toNegAndPosLitsWithRenameInfo

      public static List 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:

    • 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.

    • 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.

    • normalizeVariables

      public static String normalizeVariables(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

    • normalizeVariables

      protected static String normalizeVariables(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

    • normalizeVariables_1

      protected static String normalizeVariables_1(String input, int[] idxs, 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.

    • rename

      public Formula rename(String term2, String term1)
      Replace term2 with term1

    • substituteVariables

      public Formula substituteVariables(Map<String,String> m)
      Replace variables with a value as given by the map argument

    • extractVariables

      public static Set<String> extractVariables(Formula f)
      Extract all variables in a list

    • renameVariables

      public static Formula renameVariables(Formula f)
      convenience method

    • renameVariables

      public static Formula renameVariables(Formula f, Map topLevelVars, Map scopedRenames, Map allRenames)
      convenience method

    • universalsOut

      public static Formula universalsOut(Formula f)
      convenience method

    • getOriginalVar

      public static String getOriginalVar(String var, Map<String,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:

    • test1

      public static void test1()
      A test method.

    • testClausifier

      public static void testClausifier(String[] args)
      A test method. It expects two command line arguments for the input file and output file.

    • main

      public static void main(String[] args)