Package com.articulate.sigma
Class FormulaPreprocessor
java.lang.Object
com.articulate.sigma.FormulaPreprocessor
-
Field Summary
FieldsModifier and TypeFieldDescriptionstatic booleanstatic boolean -
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionaddTypeRestrictions(Formula form, KB kb) Add clauses for every variable in the antecedent to restrict its type to the type restrictions defined on every relation in which it appears.computeVariableTypes(Formula form, KB kb) This method returns a HashMap that maps each String variable in this the names of types (classes) of which the variable must be an instance or the names of types of which the variable must be a subclass.findAllTypeRestrictions(Formula form, KB kb) findExplicitTypes(KB kb, Formula form) Collect variable names and their types from instance or subclass expressions.voidfindExplicitTypesClasses(KB kb, Formula form, Map<String, Set<String>> varExplicitTypes, Map<String, Set<String>> varExplicitClasses) Collect variable names and their types from instance or subclass expressions.findExplicitTypesClassesInAntecedent(KB kb, Formula form) Collect the types of any variables that are specifically defined in the antecedent of a rule with an instance expression; Collect the super classes of any variables that are specifically defined in the antecedent of a rule with an subclass expression;findExplicitTypesInAntecedent(KB kb, Formula form) Collect the types of any variables that are specifically defined in the antecedent of a rule with an instance or subclass expression.static voidfindExplicitTypesRecurse(KB kb, Formula form, boolean isNegativeLiteral, Map<String, Set<String>> varExplicitTypes, Map<String, Set<String>> varExplicitClasses) Recursively collect a variable name and its types.static StringFind the argument type restriction for a given predicate and argument number that is inherited from one of its super-relations.findTypeRestrictions(Formula form, KB kb) Find all the type restrictions on the variables in a formula, including constraints from relation argument typing as well as explicitly stated types from instance and subclass expressions.protected StringgetMostRelevantType(KB kb, Set<String> types) Get the most specific type for variables.static voidpreProcess(Formula form, boolean isQuery, KB kb) Pre-process a formula before sending it to the theorem prover.replacePredVarsAndRowVars(Formula form, KB kb, boolean addHoldsPrefix) Tries to successively instantiate predicate variables and then expand row variables in this Formula, looping until no new Formulae are generated.static voidtest6()static voidstatic voidstatic voidstatic voidtestFive()static voidtestFour()static voidtestOne()static voidstatic voidtestTwo()voidwinnowTypeList(Set<String> types, KB kb) This method tries to remove all but the most specific relevant classes from a List of sortal classes.
-
Field Details
-
debug
public static boolean debug -
addOnlyNonNumericTypes
public static boolean addOnlyNonNumericTypes -
errors
-
-
Constructor Details
-
FormulaPreprocessor
public FormulaPreprocessor()
-
-
Method Details
-
findType
Find the argument type restriction for a given predicate and argument number that is inherited from one of its super-relations. A "+" is appended to the type if the parameter must be a class, meaning that a domainSubclass is defined for this argument in one of the loaded .kif files. Argument number 0 is used for the return type of a Function. Asking for a non-existent arg will return null; -
winnowTypeList
This method tries to remove all but the most specific relevant classes from a List of sortal classes.- Parameters:
types- A List of classes (class name Strings) that constrain the value of a SUO-KIF variable.kb- The KB used to determine if any of the classes in the List types are redundant.
-
findTypeRestrictions
Find all the type restrictions on the variables in a formula, including constraints from relation argument typing as well as explicitly stated types from instance and subclass expressions. -
findAllTypeRestrictions
-
addTypeRestrictions
Add clauses for every variable in the antecedent to restrict its type to the type restrictions defined on every relation in which it appears. For example (=> (foo ?A B) (bar B ?A)) (domain foo 1 Z) would result in (=> (instance ?A Z) (=> (foo ?A B) (bar B ?A))) -
getMostRelevantType
Get the most specific type for variables.- Parameters:
kb- The KB to be used for processingtypes- a list of sumo types for a sumo term/variable- Returns:
- the most specific sumo type for the term/variable For example types of ?Writing = [Entity, Physical, Process, IntentionalProcess, ContentDevelopment, Writing] return the most specific type Writing
-
findExplicitTypesInAntecedent
Collect the types of any variables that are specifically defined in the antecedent of a rule with an instance or subclass expression. TODO: This may ultimately require CNF conversion and then checking negative literals, but for now it's just a hack to grab preconditions. -
findExplicitTypesClassesInAntecedent
Collect the types of any variables that are specifically defined in the antecedent of a rule with an instance expression; Collect the super classes of any variables that are specifically defined in the antecedent of a rule with an subclass expression; -
findExplicitTypes
Collect variable names and their types from instance or subclass expressions. subclass restrictions are marked with a '+'.- Parameters:
form- The formula in KIF syntax- Returns:
- A map of variables paired with a set of sumo types collected from instance and subclass expressions. TODO: This may ultimately require CNF conversion and then checking negative literals, but for now it's just a hack to grab preconditions.
-
findExplicitTypesClasses
public void findExplicitTypesClasses(KB kb, Formula form, Map<String, Set<String>> varExplicitTypes, Map<String, Set<String>> varExplicitClasses) Collect variable names and their types from instance or subclass expressions.- Parameters:
form- The formula in KIF syntaxvarExplicitTypes- A map of variables paired with sumo types collected from instance expressionsvarExplicitClasses- A map of variables paired with sumo types collected from subclass expression
-
findExplicitTypesRecurse
public static void findExplicitTypesRecurse(KB kb, Formula form, boolean isNegativeLiteral, Map<String, Set<String>> varExplicitTypes, Map<String, Set<String>> varExplicitClasses) Recursively collect a variable name and its types. -
computeVariableTypes
This method returns a HashMap that maps each String variable in this the names of types (classes) of which the variable must be an instance or the names of types of which the variable must be a subclass. Note that this method does not capture explicit type from assertions such as (=> (instance ?Foo Bar) ...). This method just consider restrictions implicitly defined from the arg types of relations.- Parameters:
kb- The KB to be used to compute the sortal constraints for each variable.- Returns:
- A HashMap of variable names and their types. Subclass restrictions are marked with a '+', meaning that a domainSubclass is defined for this argument in one of the loaded .kif files. Instance restrictions have no special mark.
-
replacePredVarsAndRowVars
Tries to successively instantiate predicate variables and then expand row variables in this Formula, looping until no new Formulae are generated.- Parameters:
kb- The KB to be used for processing this FormulaaddHoldsPrefix- If true, predicate variables are not instantiated- Returns:
- an ArrayList of Formula(s), which could be empty.
-
preProcess
Pre-process a formula before sending it to the theorem prover. This includes ignoring meta-knowledge like documentation strings, translating mathematical operators, quoting higher-order formulas, expanding row variables and instantiating predicate variables- Parameters:
form- a formula to processisQuery- If true the Formula is a query and should be existentially quantified, else the Formula is a statement and should be universally quantifiedkb- The KB to be used for processing this Formula- Returns:
- an Set of Formula(s), which could be empty.
-
testFindTypes
public static void testFindTypes() -
testFindExplicit
public static void testFindExplicit() -
testAddTypes
public static void testAddTypes() -
testOne
public static void testOne() -
testTwo
public static void testTwo() -
testThree
public static void testThree() -
testFour
public static void testFour() -
testFive
public static void testFive() -
test6
public static void test6() -
main
-