Orbital library

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: FG.
 java.lang.Object apply(java.lang.Object I)
          Interpret this formula.
 boolean equals(java.lang.Object o)
          .
 Formula equiv(Formula B)
          Equivalence equiv: FG.
 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: FG.
 Formula not()
          Negation not: ¬F.
 Formula or(Formula B)
          Disjunction or: FG.
 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: FG.

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

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

or

Formula or(Formula B)
Disjunction or: FG.

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 FG.

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

impl

Formula impl(Formula B)
Implication impl: FG.

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

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

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

equiv

Formula equiv(Formula B)
Equivalence equiv: FG.

Sometimes this is also called bisubjunction and denoted as FG, or even FG. 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()

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.