Uses of Interface
de.uni_tuebingen.sfb.lichtenstein.formulas.Formula

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	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	SecondOrderQuantor.getArgument() Returns the formula this quantor acts on.
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	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	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	Formula.getNormalForm() Get a normal form with only conjunction, disjunction, negation and existential quantification.
Formula	BinaryJunctor.getSecondArgument() Returns the second argument.
abstract Formula	ComposedFormula.getSubformulaAt(int index) Returns the indexth subformula of this formula.
Formula	SecondOrderQuantor.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	BinaryJunctor.getSubformulaAt(int index) Returns the subformulas this binary junction is built up of.
Formula	FormulaTemplate.getTemplateFormula() Return the formula that serves as a template.
Formula	Negation.not() The negation of a negation is the formula itself.
Formula	FormulaImpl.not() Return the negation of this formula.
Formula	Formula.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	FormulaImpl.and(Formula that) Return the conjunction of this formula with that formula.
Conjunction	Formula.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.
FirstOrderExistentialQuantification	FirstOrderVariable.exists(Formula form) Returns the existential quantification of the given formula over this variable.
SecondOrderExistentialQuantification	SecondOrderVariable.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.
FirstOrderUniversalQuantification	FirstOrderVariable.forAll(Formula form) Returns the universal quantification of the given formula over this variable.
SecondOrderUniversalQuantification	SecondOrderVariable.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	FormulaImpl.iff(Formula that) Return the equivalence of this formula with that formula.
Equivalence	Formula.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	FormulaImpl.implies(Formula that) Return the implication of this formula with that formula.
Implication	Formula.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	FormulaImpl.or(Formula that) Return the disjunction of this formula with that formula.
Disjunction	Formula.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

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.

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

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.

SecondOrderUniversalQuantification(SecondOrderVariable var, Formula arg)
Initialize a new universal quantor, given a variable to bind and a formula to act upon.