|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Uses of Formula in de.uni_tuebingen.sfb.lichtenstein.binarytrees |
---|
Methods in de.uni_tuebingen.sfb.lichtenstein.binarytrees that return Formula | |
---|---|
Formula |
Query.getFormula()
Get the formula being queried. |
Methods in de.uni_tuebingen.sfb.lichtenstein.binarytrees with parameters of type Formula | |
---|---|
void |
MonaFormulaBuilder.visit(Formula form)
Visit a formula. |
Constructors in de.uni_tuebingen.sfb.lichtenstein.binarytrees with parameters of type Formula | |
---|---|
Query(Formula formula,
String treeBank,
File corporaDirectory,
File monaFileDirectory)
Initialize a Query in the given tree bank with the given formula. |
Uses of Formula in de.uni_tuebingen.sfb.lichtenstein.exceptions |
---|
Constructors in de.uni_tuebingen.sfb.lichtenstein.exceptions with parameters of type Formula | |
---|---|
FunctionArgumentsMismatchException(Formula formula,
Variable variable)
Initialize a new FunctionArgumentsMismatchException with a formula and a variable, indicating the formala does not contain the variable. |
|
VariableIndexOutOfBoundsException(Formula form,
int index)
Constructs a new VariableIndexOutOfBoundsException class with an argument indicating the illegal
index. |
Uses of Formula in de.uni_tuebingen.sfb.lichtenstein.formulas |
---|
Subinterfaces of Formula in de.uni_tuebingen.sfb.lichtenstein.formulas | |
---|---|
interface |
Quantification
A class representing a quantification. |
Classes in de.uni_tuebingen.sfb.lichtenstein.formulas that implement Formula | |
---|---|
class |
AtomicFormula
A class representing an atomic formula. |
class |
BinaryJunctor
A superclass for implication and equivalence, implementing common methods for binary junctors. |
class |
ComposedFormula
A class representing a composed formula, i.e. a formula which consists of other formulas, connected by an operator. |
class |
Conjunction
A class representing the conjunction of formulas. |
class |
Disjunction
A class representing the disjunction of formulas. |
class |
Dominance
A class representing the atomic formula which says one node dominates another. |
class |
Equivalence
A class representing the equivalence in logical formulas. |
class |
FirstOrderEquality
A class representing the atomic formula that says two first order variables are equal. |
class |
FirstOrderExistentialQuantification
A class representing the existential quantification of a formula over a first order variable. |
class |
FirstOrderQuantor
A class for representing quantors on first order variables, implementing common methods for existential and universal quantors. |
class |
FirstOrderUniversalQuantification
A class representing universal quantification of a formula over a first order variable. |
class |
FormulaImpl
A class providing implementations of the formula interface where possible. |
class |
ImmediateDominance
A class representing the atomic formula which says one node immediately dominates another. |
class |
ImmediatePrecedence
A class representing the atomic formula which says one node immediately precedes another. |
class |
Implication
A class representing the implication of formulas. |
class |
Inclusion
A class representing inclusion of a first order variable in a set denotator. |
class |
NaryJunctor
A superclass for conjunction and disjunction, implementing common methods for binary junctors. |
class |
Negation
A class representing logical negation of a formula. |
class |
Precedence
A class representing the atomic formula which says one node precedes another. |
class |
ProperDominance
A class representing the atomic formula which says one node properly dominates another. |
class |
SecondOrderEquality
A class representing the atomic formula that says two variables are equal. |
class |
SecondOrderExistentialQuantification
A class representing the existential quantification of a formula over a second order variable. |
class |
SecondOrderQuantor
A class for representing quantors on second order variables, implementing common methods for existential and universal quantors. |
class |
SecondOrderUniversalQuantification
A class representing universal quantification of a formula over a second order variable. |
class |
Subset
A class for representing the atomic formula which says a variable is a subset of another variable |
class |
UnaryJunctor
A class representing a unary junctor, having one argument. |
Methods in de.uni_tuebingen.sfb.lichtenstein.formulas that return Formula | |
---|---|
Formula |
Implication.getAntecedent()
Return the antecedent of this implication. |
Formula |
Quantification.getArgument()
Returns the formula this quantor acts on. |
Formula |
UnaryJunctor.getArgument()
Returns the argument. |
Formula |
FirstOrderQuantor.getArgument()
Returns the formula this quantor acts on. |
Formula |
SecondOrderQuantor.getArgument()
Returns the formula this quantor acts on. |
Formula |
NaryJunctor.getArgument(int index)
Get the indexth argument. |
Formula |
Implication.getConsequent()
Return the consequent of this implication. |
Formula |
BinaryJunctor.getFirstArgument()
Returns the first argument. |
Formula |
FormulaTemplate.getFormula(Variable... inputVariables)
Return the formula that results from replacing the free variables which were supplied during the creation of this template by the variables supplied as arguments to this method. |
Formula |
Negation.getNegatedFormula()
Returns the negated formula. |
Formula |
Formula.getNormalForm()
Get a normal form with only conjunction, disjunction, negation and existential quantification. |
Formula |
Negation.getNormalForm()
Get a normal form with only conjunction, disjunction, negation and existential quantification. |
Formula |
FirstOrderUniversalQuantification.getNormalForm()
Get a normal form with only conjunction, disjunction, negation and existential quantification. |
Formula |
SecondOrderUniversalQuantification.getNormalForm()
Get a normal form with only conjunction, disjunction, negation and existential quantification. |
Formula |
BinaryJunctor.getSecondArgument()
Returns the second argument. |
Formula |
BinaryJunctor.getSubformulaAt(int index)
Returns the subformulas this binary junction is built up of. |
abstract Formula |
ComposedFormula.getSubformulaAt(int index)
Returns the indexth subformula of this formula. |
Formula |
UnaryJunctor.getSubformulaAt(int index)
Returns the indexth subformula of this formula. |
Formula |
FirstOrderQuantor.getSubformulaAt(int index)
Returns the indexth subformula of this formula. |
Formula |
NaryJunctor.getSubformulaAt(int index)
Returns the indexth subformula of this formula. |
Formula |
SecondOrderQuantor.getSubformulaAt(int index)
Returns the indexth subformula of this formula. |
Formula |
FormulaTemplate.getTemplateFormula()
Return the formula that serves as a template. |
Formula |
Formula.not()
Return the negation of this formula. |
Formula |
Negation.not()
The negation of a negation is the formula itself. |
Formula |
FormulaImpl.not()
Return the negation of this formula. |
static Formula |
Formulas.not(Formula form)
Return the negation of the given formula. |
Methods in de.uni_tuebingen.sfb.lichtenstein.formulas that return types with arguments of type Formula | |
---|---|
List<Formula> |
ComposedFormula.getAllSubformulas()
Returns a list containing all subformulas of this formula. |
Methods in de.uni_tuebingen.sfb.lichtenstein.formulas with parameters of type Formula | |
---|---|
static Conjunction |
Formulas.and(Formula... forms)
Return the conjunction of the given formula with that formula. |
Conjunction |
Formula.and(Formula that)
Return the conjunction of this formula with that formula. |
Conjunction |
FormulaImpl.and(Formula that)
Return the conjunction of this formula with that formula. |
static FirstOrderExistentialQuantification |
Formulas.exists(FirstOrderVariable var,
Formula form)
Return the existential quantification of the given formula over the given first order variable. |
SecondOrderExistentialQuantification |
SecondOrderVariable.exists(Formula form)
Returns the existential quantification of the given formula over this variable. |
FirstOrderExistentialQuantification |
FirstOrderVariable.exists(Formula form)
Returns the existential quantification of the given formula over this variable. |
static SecondOrderExistentialQuantification |
Formulas.exists(SecondOrderVariable var,
Formula form)
Return the existential quantification of the given formula over the given first order variable. |
static FirstOrderUniversalQuantification |
Formulas.forAll(FirstOrderVariable var,
Formula form)
Return the universal quantification of the given formula over the given variable. |
SecondOrderUniversalQuantification |
SecondOrderVariable.forAll(Formula form)
Returns the universal quantification of the given formula over this variable. |
FirstOrderUniversalQuantification |
FirstOrderVariable.forAll(Formula form)
Returns the universal quantification of the given formula over this variable. |
static SecondOrderUniversalQuantification |
Formulas.forAll(SecondOrderVariable var,
Formula form)
Return the universal quantification of the given formula over the given variable. |
boolean |
NaryJunctor.hasAsArgument(Formula form)
Returns whether this n-ary junctor has the given formula as an argument. |
Equivalence |
Formula.iff(Formula that)
Return the equivalence of this formula with that formula. |
Equivalence |
FormulaImpl.iff(Formula that)
Return the equivalence of this formula with that formula. |
static Equivalence |
Formulas.iff(Formula first,
Formula second)
Return the equivalence of the given formula with that formula. |
Implication |
Formula.implies(Formula that)
Return the implication of this formula with that formula. |
Implication |
FormulaImpl.implies(Formula that)
Return the implication of this formula with that formula. |
static Implication |
Formulas.implies(Formula first,
Formula second)
Return the implication of the first formula with the second formula. |
static Formula |
Formulas.not(Formula form)
Return the negation of the given formula. |
static Disjunction |
Formulas.or(Formula... forms)
Return the disjunction of the given formula with second formula. |
Disjunction |
Formula.or(Formula that)
Return the disjunction of this formula with that formula. |
Disjunction |
FormulaImpl.or(Formula that)
Return the disjunction of this formula with that formula. |
abstract void |
FormulaVisitor.visit(Formula form)
Visit a formula. |
Constructors in de.uni_tuebingen.sfb.lichtenstein.formulas with parameters of type Formula | |
---|---|
BinaryJunctor(Formula first,
Formula second)
Initialize a new binary junctor, taking two formulas as arguments. |
|
Conjunction(Formula... arguments)
Initialize a new conjunction, taking formulas as conjuncts. |
|
Disjunction(Formula... arguments)
Initialize a new disjunction, taking formulas as disjuncts. |
|
Equivalence(Formula first,
Formula second)
Initialize a new equivalence between two formulas. |
|
FirstOrderExistentialQuantification(FirstOrderVariable var,
Formula arg)
Initialize a new existential quantor, given a variable to bind and a formula to act upon. |
|
FirstOrderQuantor(FirstOrderVariable var,
Formula arg)
Initialize a new quantor, given a variable to bind and a formula to act upon. |
|
FirstOrderUniversalQuantification(FirstOrderVariable var,
Formula arg)
Initialize a new universal quantor, given a variable to bind and a formula to act upon. |
|
FormulaTemplate(Formula template,
Variable... dummies)
Initialize a new formula template, based on a formula and a list of dummy variables that appear in the formula. |
|
Implication(Formula antecedent,
Formula consequent)
Initialize a new implication, given an antecedent and a consequent |
|
NaryJunctor(Formula... arguments)
Initialize a new n-ary junctor, taking an unlimited number of formulas as arguments. |
|
Negation(Formula negatedFormula)
Initialize a new negation, given the formula to be negated. |
|
SecondOrderExistentialQuantification(SecondOrderVariable var,
Formula arg)
Initialize a new existential quantor, given a variable to bind and a formula to act upon. |
|
SecondOrderQuantor(SecondOrderVariable var,
Formula arg)
Initialize a new quantor, given a variable to bind and a formula to act upon. |
|
SecondOrderUniversalQuantification(SecondOrderVariable var,
Formula arg)
Initialize a new universal quantor, given a variable to bind and a formula to act upon. |
|
UnaryJunctor(Formula argument)
Initialize a new unary junctor, taking a formula as argument. |
Uses of Formula in de.uni_tuebingen.sfb.lichtenstein.formulas.parsing |
---|
Methods in de.uni_tuebingen.sfb.lichtenstein.formulas.parsing that return Formula | |
---|---|
Formula |
fsqParser.atomic()
|
Formula |
fsqParser.binary()
|
Formula |
fsqParser.body()
|
Formula |
fsqParser.containment()
|
Formula |
fsqParser.dominance()
|
Formula |
fsqParser.equality()
|
Formula |
fsqParser.formula()
|
Formula |
fsqParser.immediateDominance()
|
Formula |
fsqParser.immediatePrecedence()
|
Formula |
fsqParser.labelFormula()
|
Formula |
fsqParser.n_ary()
|
Formula |
fsqParser.precedence()
|
Formula |
fsqParser.properDominance()
|
Formula |
fsqParser.quantor()
|
Formula |
fsqParser.unary()
|
Methods in de.uni_tuebingen.sfb.lichtenstein.formulas.parsing that return types with arguments of type Formula | |
---|---|
List<Formula> |
fsqParser.n_aryArguments()
|
Uses of Formula in de.uni_tuebingen.sfb.lichtenstein.UI |
---|
Constructors in de.uni_tuebingen.sfb.lichtenstein.UI with parameters of type Formula | |
---|---|
ResultView(List<Sentence> results,
Formula query,
Action quitAction)
Initialize a new result view with the given results. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |