Uses of Interface
orbital.logic.imp.Formula

Packages that use Formula

orbital.logic.imp	Defines a generic interface to (symbolic) logic systems.
orbital.moon.logic	Contains implementations of some logics as well as a logic and mathematical expression parser.
orbital.moon.logic.resolution	Provides resolution inference theorem prover implementation and clause management.

Uses of Formula in orbital.logic.imp

Subinterfaces of Formula in orbital.logic.imp

static interface

Formula.Composite Interface for composite formulas.

Classes in orbital.logic.imp that implement Formula

class

LogicBasis This abstract LogicBasis class derives the extended logic operations depending upon basic logic operations.

Methods in orbital.logic.imp that return Formula

Formula	Formula.and(Formula B) Conjunction and: F ∧ G.
Formula	LogicBasis.equiv(Formula B) Equivalence equiv: A ⇔ B is calced (A→B) ∧ (B→A)
Formula	Formula.equiv(Formula B) Equivalence equiv: F ↔ G.
Formula	LogicBasis.exists(Symbol x) Existence-quantifier exists: ∃x A is calced ¬∀x ¬A.
Formula	Formula.exists(Symbol x) Existential-quantifier exists: ∃x F.
Formula	LogicBasis.forall(Symbol x) All-quantifier forall: ∀x A is calced ¬∃x ¬A.
Formula	Formula.forall(Symbol x) Universal-quantifier forall: ∀x F.
Formula	LogicBasis.impl(Formula B) Implication impl: A → B is calced ¬A ∨ B
Formula	Formula.impl(Formula B) Implication impl: F → G.
Formula	Formula.not() Negation not: ¬F.
Formula	Formula.or(Formula B) Disjunction or: F ∨ G.
Formula	LogicBasis.xor(Formula B) Exclusion xor: A xor B is calced (A∧¬B) ∨ (¬A∧B)
Formula	Formula.xor(Formula B) Exclusion xor: F ∨̇ G = F xor G.

Methods in orbital.logic.imp with parameters of type Formula

Formula	Formula.and(Formula B) Conjunction and: F ∧ G.
Formula	LogicBasis.equiv(Formula B) Equivalence equiv: A ⇔ B is calced (A→B) ∧ (B→A)
Formula	Formula.equiv(Formula B) Equivalence equiv: F ↔ G.
Formula	LogicBasis.impl(Formula B) Implication impl: A → B is calced ¬A ∨ B
Formula	Formula.impl(Formula B) Implication impl: F → G.
boolean	Inference.infer(Formula[] w, Formula d) Apply the inference relation |~ according to the implementation calculus K.
boolean	Inference.infer(Formula[] w, Formula d) Apply the inference relation |~ according to the implementation calculus K.
Formula	Formula.or(Formula B) Disjunction or: F ∨ G.
boolean	Logic.satisfy(Interpretation I, Formula F) Defines the semantic satisfaction relation ⊧.
Formula	LogicBasis.xor(Formula B) Exclusion xor: A xor B is calced (A∧¬B) ∨ (¬A∧B)
Formula	Formula.xor(Formula B) Exclusion xor: F ∨̇ G = F xor G.

Uses of Formula in orbital.moon.logic

Methods in orbital.moon.logic that return Formula

static Formula	ClassicalLogic.Utilities.conjunctiveForm(Formula f) Transforms into conjunctive normal form (CNF).
static Formula	ClassicalLogic.Utilities.conjunctiveForm(Formula f, boolean simplifying) Transforms into conjunctive normal form (CNF).
static Formula	ClassicalLogic.Utilities.constantClosure(Formula F) Get the constant-closure of a formula.
Formula	ClassicalLogic.createFormula(java.lang.String expression) Deprecated. Use (Formula) createExpression(expression) instead.
static Formula	ClassicalLogic.Utilities.disjunctiveForm(Formula f) Transforms into disjunctive normal form (DNF).
static Formula	ClassicalLogic.Utilities.disjunctiveForm(Formula f, boolean simplifying) Transforms into disjunctive normal form (DNF).
static Formula	ClassicalLogic.Utilities.dropQuantifiers(Formula F) Drop any quantifiers.
static Formula	ClassicalLogic.Utilities.existentialClosure(Formula F) Get the ∃-closure of a formula.
static Formula	ClassicalLogic.Utilities.negation(Formula F) Get the negation of F without introducing duplex negatios.
static Formula	ClassicalLogic.Utilities.negationForm(Formula F) Get the negation normal form of a formula.
static Formula	ClassicalLogic.Utilities.skolemForm(Formula F) Get the Skolem normal form of a formula.
static Formula	ClassicalLogic.Utilities.universalClosure(Formula F) Get the ∀-closure of a formula.

Methods in orbital.moon.logic with parameters of type Formula

static java.util.Set	ClassicalLogic.Utilities.clausalForm(Formula f, boolean simplifying) Deprecated. Prefer to use the more general method ClausalFactory.asClausalSet(orbital.logic.imp.Formula) instead.
static Formula	ClassicalLogic.Utilities.conjunctiveForm(Formula f) Transforms into conjunctive normal form (CNF).
static Formula	ClassicalLogic.Utilities.conjunctiveForm(Formula f, boolean simplifying) Transforms into conjunctive normal form (CNF).
static Formula	ClassicalLogic.Utilities.constantClosure(Formula F) Get the constant-closure of a formula.
static Formula	ClassicalLogic.Utilities.disjunctiveForm(Formula f) Transforms into disjunctive normal form (DNF).
static Formula	ClassicalLogic.Utilities.disjunctiveForm(Formula f, boolean simplifying) Transforms into disjunctive normal form (DNF).
static Formula	ClassicalLogic.Utilities.dropQuantifiers(Formula F) Drop any quantifiers.
static Formula	ClassicalLogic.Utilities.existentialClosure(Formula F) Get the ∃-closure of a formula.
static Formula	ClassicalLogic.Utilities.negation(Formula F) Get the negation of F without introducing duplex negatios.
static Formula	ClassicalLogic.Utilities.negationForm(Formula F) Get the negation normal form of a formula.
boolean	ModalLogic.satisfy(Interpretation I, Formula F)
boolean	FuzzyLogic.satisfy(Interpretation I, Formula F)
boolean	ClassicalLogic.satisfy(Interpretation I, Formula F)
static Formula	ClassicalLogic.Utilities.skolemForm(Formula F) Get the Skolem normal form of a formula.
static Formula	ClassicalLogic.Utilities.universalClosure(Formula F) Get the ∀-closure of a formula.

Uses of Formula in orbital.moon.logic.resolution

Methods in orbital.moon.logic.resolution that return Formula

Formula	ClauseImpl.toFormula()
Formula	Clause.toFormula() Convert this clause to a formula representation.
Formula	ClausalSetImpl.toFormula()
Formula	ClausalSet.toFormula() Convert this set of clauses to a formula representation.

Methods in orbital.moon.logic.resolution with parameters of type Formula

ClausalSet	DefaultClausalFactory.asClausalSet(Formula f)
ClausalSet	ClausalFactory.asClausalSet(Formula formula) Returns a clausal set representation of the given formula.
java.util.Iterator	ClausalIndex.getProbableComplementClauses(Formula L) Get an iterator of all clauses that contain literals which could possibly unify with ~L.
java.util.Iterator	ClausalIndex.getProbableComplementLiterals(Formula L) Get an iterator of all literals which could possibly unify with ~L.
java.util.Iterator	ClausalIndex.getProbableComplements(Formula L) Get an iterator of all (clause,literal) pairs which could possibly unify with ~L.
java.util.Iterator	ClausalIndex.getProbableUnifiableClauses(Formula L) Get an iterator of all clauses that contain literals which could possibly unify with L.
java.util.Iterator	ClausalIndex.getProbableUnifiableLiterals(Formula L) Get an iterator of all literals which could possibly unify with L.
java.util.Iterator	OrderedClauseImpl.getProbableUnifiables(Formula L)
java.util.Iterator	IndexedClauseImpl.getProbableUnifiables(Formula L)
java.util.Iterator	IndexedClausalSetImpl.getProbableUnifiables(Formula L) Get an iterator of all clauses that contain literals which could possibly unify with L.
java.util.Iterator	ClauseImpl.getProbableUnifiables(Formula L)
java.util.Iterator	Clause.getProbableUnifiables(Formula L) Get (an iterator over) all literals contained in this clause that may possibly unify with L.
java.util.Iterator	ClausalIndex.getProbableUnifiables(Formula L) Get an iterator of all (clause,literal) pairs which could possibly unify with L.
java.util.Set	ClauseImpl.getUnifiables(Formula L)
java.util.Set	Clause.getUnifiables(Formula L) Get all literals contained in this clause that unify with L.
boolean	ResolutionBase.infer(Formula[] B, Formula D) Apply the inference relation |~ according to the implementation calculus K.
boolean	ResolutionBase.infer(Formula[] B, Formula D) Apply the inference relation |~ according to the implementation calculus K.
protected Clause	OrderedClauseImpl.resolventWith(Clause _G, Formula L, Formula K)
protected Clause	ClauseImpl.resolventWith(Clause G, Formula L, Formula K) Resolve clause F with G by the complementary resolution literals L∈F and K∈G.
protected Pair	ClauseImpl.resolventWith2(Clause G, Formula L, Formula K) Workaround for returning 2 arguments.