
Orbital library  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
public interface Formula
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.
Cl_{∀}
F is validCl_{∃}
F is satisfiableshort  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 
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.
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 247248. Oxford University Press. 1994"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)
Existentialquantifier exists: ∃x F. 
Formula 
forall(Symbol x)
Universalquantifier 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 

boolean equals(java.lang.Object o)
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.
equals
in interface Functor
equals
in class java.lang.Object
int hashCode()
hashCode
in interface Functor
hashCode
in class java.lang.Object
java.util.Set getFreeVariables()
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(t_{1},...,t_{n})) 
= FV(t_{1}) ∪...∪ FV(t_{n}) 
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(t_{1},...,t_{n})) 
= FV(t_{1}) ∪...∪ FV(t_{n}) 
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.
java.util.Set getBoundVariables()
bound variables BV(F) of a formula F∈Formula(Σ) with V⊆Σ being the set of variables are:
BV:Formula(Σ)→℘(V); 

BV(P(t_{1},...,t_{n})) 
= ∅ 
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 
java.util.Set getVariables()
getFreeVariables()
,
getBoundVariables()
java.lang.Object apply(java.lang.Object I)
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.
apply
in interface Function
I
 the interpretation I.
Logic.satisfy(Interpretation, Formula)
Formula not()
java.lang.UnsupportedOperationException
 if this junctor is not supported by the representation.Formula and(Formula B)
Also denoted as F & G. Sometimes even as F G, F.G, K FG.
java.lang.UnsupportedOperationException
 if this junctor is not supported by the representation.Formula or(Formula B)
Sometimes also denoted as A FG.
java.lang.UnsupportedOperationException
 if this junctor is not supported by the representation.Formula xor(Formula B)
Xor is also called antivalence and sometimes denoted as F ↮ G.
java.lang.UnsupportedOperationException
 if this junctor is not supported by the representation.Formula impl(Formula B)
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.
java.lang.UnsupportedOperationException
 if this junctor is not supported by the representation.Formula equiv(Formula B)
Sometimes this is also called bisubjunction and denoted as F ⇔ G, or even F ≡ G. Sometimes also denoted as E FG.
java.lang.UnsupportedOperationException
 if this junctor is not supported by the representation.Formula forall(Symbol x)
Sometimes, this is also denoted as ⋀_{x} F.
∀ is not (compositional or) truthfunctional.
x
 is a symbol x for all elements of the world.
java.lang.UnsupportedOperationException
 if this quantifier is not supported by the representation.Formula exists(Symbol x)
Sometimes, this is also denoted as ⋁_{x} F.
∀ is not (compositional or) truthfunctional.
x
 is a symbol x for an element of the world.
java.lang.UnsupportedOperationException
 if this quantifier is not supported by the representation.

Orbital library 1.3.0: 11 Apr 2009 

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 