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 Formulaextends 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
`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).
`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).
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