orbital.logic.imp
Interface Formula

All Superinterfaces:

Expression, Function, Functor, Typed

All Known Subinterfaces:

Formula.Composite

All Known Implementing Classes:

LogicBasis

public interface Formula
extends Expression, Function

A formula interface for presentations of formal logic. This interface also defines an encapsulation for basic logic junction operations (called junctors). Logic representations must balance expressiveness and tractability.

Objects representing compound formulas implement Formula.Composite, which can be used for decomposition and analysis of compound formulas.

Formulas can formally be classified with these essential characteristics. With F∈Formula(Σ) the formula F is:

valid (or tautological or universal or necessary or analytical)

if Mod_Σ(F)=Int(Σ), that is, if it is satisfied by all interpretations. A formula is tautological, if it is not falsifiable.

⇔ Cl∀ F is valid

satisfiable (or consistent or possible)

if Mod_Σ(F)≠∅, that is, if it is satisfied by at least one interpretation (together with a variable assignement).

⇔ C({F}) ≠ Formula(Σ)

⇔ F ⊭ false

⇔ there is no A∈Formula(Σ) with F ⊨ A and F ⊨ ¬A

⇔ F has a class of models

⇔ Cl∃ F is satisfiable

falsifiable

if Mod_Σ(F)≠Int(Σ), that is, if it is falsified by at least one interpretation.

unsatisfiable (or inconsistent)

A formula is inconsistent, if it is not consistent, i.e. if Mod_Σ(F)=∅, that is, if it is falsified by all interpretations.

complete

if for all closed A∈Formula(Σ) it is F ⊨ A or F ⊨ ¬A

⇔ F has at most one class of models

Table of essential characteristics of formulas

short	prosa	models	prosa
⊨ F	F is valid	ModΣ(F)=Int(Σ)	all models
⊭ ¬F	F is satisfiable	ModΣ(F)≠∅	some models
⊭ F	F is falsifiable	ModΣ(F)≠Int(Σ)	not all models
⊨ ¬F	F is unsatisfiable	ModΣ(F)=∅	no models

Satisfying models are interpretations that satisfy the formula. All these definitions generalize to sets of formulas F instead of a single formula F.

Formulas are simply algebraic expressions, which define functions over individiuals of a universe. Whereas logical junctors define functions over truth values, and quantifiers define higher order functions, instead. However, note that it is not an inherent property that formulas extend Function, but a matter of modelling. This view leads to an attracting simplicity, although there is not necessarily a semantical connection categorizing formulas as functions. The relation between formulas and functions is not necessarily one of specialization, but of adopting a certain part of functions' behaviour under a single aspect. An important advantage of this decision is that the machinery developed for logical functions, like composition, binding etc. can be applied to (composed) formulas, as well. Calling the formula's apply(Object) method will get the value of this formula, given an interpretation that is passed as an argument.

Author:

André Platzer

See Also:

Inference.infer(orbital.logic.imp.Formula[], orbital.logic.imp.Formula), LogicBasis, ExpressionBuilder.createAtomic(Symbol), Interpreter, "Daniel Leivant. Higher order logic, Chapter 3.6 Formulas as higher order functions. In: Dov M. Gabbay, editor, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 247-248. Oxford University Press. 1994"

Structure:

extends Expression, extends Function

Note:

boolean formulas (of propositional logic) can also be represented with (reduced) OBDDs, for performance in some applications.

Nested Class Summary

static interface

Formula.Composite Interface for composite formulas.

Nested classes/interfaces inherited from interface orbital.logic.functor.Functor

Functor.Specification

Field Summary

Fields inherited from interface orbital.logic.functor.Function

callTypeDeclaration

Method Summary

Formula	and(Formula B) Conjunction and: F ∧ G.
java.lang.Object	apply(java.lang.Object I) Interpret this formula.
boolean	equals(java.lang.Object o) .
Formula	equiv(Formula B) Equivalence equiv: F ↔ G.
Formula	exists(Symbol x) Existential-quantifier exists: ∃x F.
Formula	forall(Symbol x) Universal-quantifier forall: ∀x F.
java.util.Set	getBoundVariables() Get the set of the bound variables of this formula.
java.util.Set	getFreeVariables() Get the set of the free variables of this formula.
java.util.Set	getVariables() Get the set of all variables of this formula.
int	hashCode()
Formula	impl(Formula B) Implication impl: F → G.
Formula	not() Negation not: ¬F.
Formula	or(Formula B) Disjunction or: F ∨ G.
Formula	xor(Formula B) Exclusion xor: F ∨̇ G = F xor G.

Methods inherited from interface orbital.logic.sign.Expression

getSignature

Methods inherited from interface orbital.logic.sign.type.Typed

getType

Methods inherited from interface orbital.logic.functor.Functor

toString

Method Detail

equals

boolean equals(java.lang.Object o)

Description copied from interface: Functor

.

Note that functors will often provide intensional equality only, since the mathematical notion of extensional equality for functions and predicates is undecidable anyway (Proposition of Rice). Nevertheless implementations are encouraged to provide a larger subset of extensional equality as far as possible.

Specified by:

equals in interface Functor

Overrides:

equals in class java.lang.Object

hashCode

int hashCode()

Specified by:

hashCode in interface Functor

Overrides:

hashCode in class java.lang.Object

getFreeVariables

java.util.Set getFreeVariables()

Get the set of the free variables of this formula.

free variables FV(t) of a term t∈Term(Σ) with V⊆Σ being the set of variables are:

FV:Term(Σ)→℘(V);
	FV(x)	= {x}	if x∈V
	FV(f(t1,...,tn))	= FV(t1) ∪...∪ FV(tn)	if f∈Func/n
	FV(c)	= ∅	if c∈Func/0

free variables FV(F) of a formula F∈Formula(Σ) with V⊆Σ being the set of variables are:

FV:Formula(Σ)→℘(V);
	FV(P(t1,...,tn))	= FV(t1) ∪...∪ FV(tn)	if P∈Pred/n
	FV(¬G)	= FV(G)
	FV(G ⋆ H)	= FV(G) ∪ FV(H)	⋆∈{∧,∨,⇒,⇔}
	FV(@xG)	= FV(G) ∖ {x}	if bound by a @∈{∀,∃}
	FV(P)	= ∅	if P∈Pred/0

A formula F is ground or closed if it holds no free variables FV(F) = ∅, or open if it has free variables FV(F) ≠ ∅.

A formula F can be closed by the universal closure Cl_∀(F), and the existence closure Cl_∃(F) which bind all free variables of F by ∀ resp. ∃ quantifiers.

Returns:

FV(this).

getBoundVariables

java.util.Set getBoundVariables()

Get the set of the bound variables of this formula.

bound variables BV(F) of a formula F∈Formula(Σ) with V⊆Σ being the set of variables are:

BV:Formula(Σ)→℘(V);
	BV(P(t1,...,tn))	= ∅	if P∈Pred/n
	BV(¬G)	= BV(G)
	BV(G ⋆ H)	= BV(G) ∪ BV(H)	⋆∈{∧,∨,⇒,⇔}
	BV(@xG)	= BV(G) ∪ {x}	if bound by a @∈{∀,∃}
	BV(P)	= ∅	if P∈Pred/0

Returns:

BV(this).

getVariables

java.util.Set getVariables()

Get the set of all variables of this formula.

Returns:

V(this) := FV(this)∪BV(this).

See Also:

getFreeVariables(), getBoundVariables()

apply

java.lang.Object apply(java.lang.Object I)

Interpret this formula.

Note that this method may choose to ignore any changes in the core interpretations, and stick to the core interpretation at the time of formula construction. The later may be ensured by formulas of fixed interpretations.

Specified by:

apply in interface Function

Parameters:

I - the interpretation I.

Returns:

I(this).

See Also:

Interpreter, "Visitor", Logic.satisfy(Interpretation, Formula)

not

Formula not()

Negation not: ¬F.

Throws:

java.lang.UnsupportedOperationException - if this junctor is not supported by the representation.

and

Formula and(Formula B)

Conjunction and: F ∧ G.

Also denoted as F & G. Sometimes even as F G, F.G, K FG.

Throws:

java.lang.UnsupportedOperationException - if this junctor is not supported by the representation.

or

Formula or(Formula B)

Disjunction or: F ∨ G.

Sometimes also denoted as A FG.

Throws:

java.lang.UnsupportedOperationException - if this junctor is not supported by the representation.

xor

Formula xor(Formula B)

Exclusion xor: F ∨̇ G = F xor G.

Xor is also called antivalence and sometimes denoted as F ↮ G.

Throws:

java.lang.UnsupportedOperationException - if this junctor is not supported by the representation.

impl

Formula impl(Formula B)

Implication impl: F → G.

This implication is also called subjunction and denoted as F ⊃ G. Sometimes implication is also denoted as F ⇒ G to underline that it is a material implications. Sometimes also denoted as C FG.

¬G→¬F is called contra position of F→G. G→F is called reciprocal of F→G.

Throws:

java.lang.UnsupportedOperationException - if this junctor is not supported by the representation.

equiv

Formula equiv(Formula B)

Equivalence equiv: F ↔ G.

Sometimes this is also called bisubjunction and denoted as F ⇔ G, or even F ≡ G. Sometimes also denoted as E FG.

Throws:

java.lang.UnsupportedOperationException - if this junctor is not supported by the representation.

forall

Formula forall(Symbol x)

Universal-quantifier forall: ∀x F.

Sometimes, this is also denoted as ⋀_x F.

∀ is not (compositional or) truth-functional.

Parameters:

x - is a symbol x for all elements of the world.

Throws:

java.lang.UnsupportedOperationException - if this quantifier is not supported by the representation.

Preconditions:

x.isVariable()

exists

Formula exists(Symbol x)

Existential-quantifier exists: ∃x F.

Sometimes, this is also denoted as ⋁_x F.

∀ is not (compositional or) truth-functional.

Parameters:

x - is a symbol x for an element of the world.

Throws:

java.lang.UnsupportedOperationException - if this quantifier is not supported by the representation.

Preconditions:

x.isVariable()