org.qedeq.kernel.bo.logic.common
Class FormulaUtility

java.lang.Object
  org.qedeq.kernel.bo.logic.common.FormulaUtility

All Implemented Interfaces:

Operators

public final class FormulaUtility
extends java.lang.Object
implements Operators

Some useful static methods for formulas and terms.

Author:

Michael Meyling

Field Summary

Fields inherited from interface org.qedeq.kernel.bo.logic.common.Operators

CLASS_OP, CONJUNCTION_OPERATOR, DISJUNCTION_OPERATOR, EQUIVALENCE_OPERATOR, EXISTENTIAL_QUANTIFIER_OPERATOR, FUNCTION_CONSTANT, FUNCTION_VARIABLE, IMPLICATION_OPERATOR, META_VARIABLE, NEGATION_OPERATOR, PREDICATE_CONSTANT, PREDICATE_VARIABLE, SUBJECT_VARIABLE, UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR, UNIVERSAL_QUANTIFIER_OPERATOR

Method Summary

static boolean	containsOperatorVariable(Element formula, Element operatorVariable) Checks if a given term or formula contains a given function or predicate variable with same size.
static Element	createMeta(Element subjectVariable) Create meta variable for subject variable.
static Element	createPredicateVariable(java.lang.String predicateVariableName) Create predicate variable out of variable name with no further arguments.
static Element	createSubjectVariable(java.lang.String subjectVariableName) Create subject variable out of variable name.
static ElementSet	getBoundSubjectVariables(Element element) Return all bound subject variables of an element.
static java.lang.String	getDifferenceLocation(Element first, Element second) Get relative context of the first difference between the given elements.
static ElementSet	getFreeSubjectVariables(Element element) Return all free subject variables of an element.
static ElementSet	getPartFormulas(Element element) Return all part formulas of an element.
static ElementSet	getPredicateVariables(Element element) Return all predicate variables of an element.
static ElementSet	getPropositionVariables(Element element) Return all proposition variables of an element.
static ElementSet	getSubjectVariables(Element element) Return all subject variables of an element.
static boolean	isBindingOperator(ElementList list) Has the given list an operator that binds a subject variable?
static boolean	isFunctionConstant(Element element) Is Element a function constant?
static boolean	isFunctionVariable(Element element) Is Element a function variable?
static boolean	isImplication(Element formula) Is the given formula a simple implication like A => B.
static boolean	isOperator(java.lang.String operator, Element element) Is the given element an list with given operator and has as first element an non empty string atom?
static boolean	isPredicateConstant(Element element) Is Element a predicate constant?
static boolean	isPredicateVariable(Element element) Is Element a predicate variable?
static boolean	isPropositionVariable(Element element) Is Element a proposition variable?
static boolean	isSubjectVariable(Element element) Is Element a subject variable?
static Element	replaceOperatorVariable(Element formula, Element operatorVariable, Element replacement) Replace function or predicate variable by given term or formula.
static Element	replaceSubjectVariableQuantifier(Element originalSubjectVariable, Element replacementSubjectVariable, Element formulaElement, int occurrenceGoal, Enumerator occurreneCurrent) Replace bound subject variables at given occurrence by another one.
static boolean	testOperatorVariable(Element formula, Element operatorVariable, ElementSet bound) Test if operator occurrence in formula matches always to a formula that contains no subject variable that is in the given ElementSet of bound subject variables..

Methods inherited from class java.lang.Object

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

Method Detail

isSubjectVariable

public static final boolean isSubjectVariable(Element element)

Is Element a subject variable?

Parameters:

element - Element to look onto.

Returns:

Is it a subject variable?

isPredicateVariable

public static final boolean isPredicateVariable(Element element)

Is Element a predicate variable?

Parameters:

element - Element to look onto.

Returns:

Is it a predicate variable?

isPropositionVariable

public static final boolean isPropositionVariable(Element element)

Is Element a proposition variable?

Parameters:

element - Element to look onto.

Returns:

Is it a proposition variable?

isFunctionVariable

public static final boolean isFunctionVariable(Element element)

Is Element a function variable?

Parameters:

element - Element to look onto.

Returns:

Is it a function variable?

isPredicateConstant

public static final boolean isPredicateConstant(Element element)

Is Element a predicate constant?

Parameters:

element - Element to look onto.

Returns:

Is it a predicate constant?

isFunctionConstant

public static final boolean isFunctionConstant(Element element)

Is Element a function constant?

Parameters:

element - Element to look onto.

Returns:

Is it a function constant?

isOperator

public static boolean isOperator(java.lang.String operator,
                                 Element element)

Is the given element an list with given operator and has as first element an non empty string atom?

Parameters:

operator - Operator.

element - Check this element.

Returns:

Check successful?

getFreeSubjectVariables

public static final ElementSet getFreeSubjectVariables(Element element)

Return all free subject variables of an element.

Parameters:

element - Work on this element.

Returns:

All free subject variables.

getBoundSubjectVariables

public static final ElementSet getBoundSubjectVariables(Element element)

Return all bound subject variables of an element.

Parameters:

element - Work on this element.

Returns:

All bound subject variables.

getSubjectVariables

public static final ElementSet getSubjectVariables(Element element)

Return all subject variables of an element.

Parameters:

element - Work on this element.

Returns:

All subject variables.

getPredicateVariables

public static final ElementSet getPredicateVariables(Element element)

Return all predicate variables of an element. The arguments are normalized to subject variables "x_1", "x_2" and so on.

Parameters:

element - Work on this element.

Returns:

All predicate variables of that formula.

getPropositionVariables

public static final ElementSet getPropositionVariables(Element element)

Return all proposition variables of an element. That are predicate variables with arity zero.

Parameters:

element - Work on this element.

Returns:

All proposition variables of that formula.

getPartFormulas

public static final ElementSet getPartFormulas(Element element)

Return all part formulas of an element.

Parameters:

element - Work on this element.

Returns:

All part formulas of that element.

isBindingOperator

public static boolean isBindingOperator(ElementList list)

Has the given list an operator that binds a subject variable?

Parameters:

list - Check for this operator.

Returns:

Has it an binding operator with subject variable?

getDifferenceLocation

public static java.lang.String getDifferenceLocation(Element first,
                                                     Element second)

Get relative context of the first difference between the given elements.

Parameters:

first - First element.

second - Second element.

Returns:

Relative path (beginning with ".") of first difference.

replaceSubjectVariableQuantifier

public static Element replaceSubjectVariableQuantifier(Element originalSubjectVariable,
                                                       Element replacementSubjectVariable,
                                                       Element formulaElement,
                                                       int occurrenceGoal,
                                                       Enumerator occurreneCurrent)

Replace bound subject variables at given occurrence by another one. If goal occurrence number is below number of occurrences within the formula nothing is changed. Original parts are used, so don't modify the formulas directly.

Parameters:

originalSubjectVariable - Replace this subject variable.

replacementSubjectVariable - By this subject variable.

formulaElement - This is the formula we work on.

occurrenceGoal - This is the binding occurrence number.

occurreneCurrent - Counter how much occurrences we already had.

Returns:

Formula with replaced subject variables.

replaceOperatorVariable

public static Element replaceOperatorVariable(Element formula,
                                              Element operatorVariable,
                                              Element replacement)

Replace function or predicate variable by given term or formula. Old parts are not copied but taken directly - so don't modify the formulas!

Parameters:

formula - Formula we want the replacement take place.

operatorVariable - Predicate variable or function variable with only subject variables as arguments.

replacement - Replacement formula or term with matching subject variables. operatorVariable might have some subject variables that are not in replacement and vice versa.

Returns:

Formula where operatorVariable was replaced.

containsOperatorVariable

public static boolean containsOperatorVariable(Element formula,
                                               Element operatorVariable)

Checks if a given term or formula contains a given function or predicate variable with same size.

Parameters:

formula - Formula we want the replacement take place.

operatorVariable - Predicate variable or function variable with only subject variables as arguments.

Returns:

Do we have any occurrence?

testOperatorVariable

public static boolean testOperatorVariable(Element formula,
                                           Element operatorVariable,
                                           ElementSet bound)

Test if operator occurrence in formula matches always to a formula that contains no subject variable that is in the given ElementSet of bound subject variables..

Parameters:

formula - Formula we want to test the condition.

operatorVariable - Predicate variable or function variable with only subject variables as arguments.

bound - Set of subject variables that are tabu.

Returns:

Formula test was successful.

isImplication

public static boolean isImplication(Element formula)

Is the given formula a simple implication like A => B.

Parameters:

formula - Check this formula.

Returns:

Is the formula a simple implication?

createMeta

public static Element createMeta(Element subjectVariable)

Create meta variable for subject variable.

Parameters:

subjectVariable - Subject variable, we want to have a meta variable for.

Returns:

Resulting meta variable. If we didn't got a subject variable we just return the original.

createSubjectVariable

public static Element createSubjectVariable(java.lang.String subjectVariableName)

Create subject variable out of variable name.

Parameters:

subjectVariableName - Subject variable name.

Returns:

Resulting subject variable.

createPredicateVariable

public static Element createPredicateVariable(java.lang.String predicateVariableName)

Create predicate variable out of variable name with no further arguments.

Parameters:

predicateVariableName - Predicate variable name.

Returns:

Resulting predicate variable.