orbital.logic.imp
Interface Inference
 All Known Implementing Classes:
 ResolutionBase, SaturationResolution, SearchResolution, SetOfSupportResolution
public interface Inference
Provides a unified encapsulation for inference relations ~ used for any logic reasoning.
It encapsulates a general inference relation:
~ ⊆ ℘(Formula(Σ))×Formula(Σ)
An inference relation is a relation between existing knowledge and the knowledge to be derived.
Every inference over syntactic symbols of the representation must preserve structure
for the elements of the world represented.
Usually, ~ treats nonlogical terminology
as implicitly bound free variables.
The intuition of an inference W ~ F
to hold is that
on the basis of the set of formulas W known (or assumed) to be true
one can conclude that F∈Formula(Σ) is true as well.
(See below for a constructive definition applicable in most cases).
Often, the signature Σ is not specified if it is implicitly obvious from the context.
 inference operation of ~

An inference operation that belongs to an inference relation ~
can be defined as the consequence closure
C: ℘(Formula(Σ))→℘(Formula(Σ)); W↦C(W) := {F∈Formula(Σ) ¦ W ~ F}
 deductively closed

A set of formulas F is called deductively closed if it is a fixed point of C
C(F) = F
Inference relations of a logic can formally be classified with these properties
of the corresponding inference operation C.
The inference relation ~ is:
 reflexive
 if A⊆C(A).
 cut
 if A⊆B⊆C(A) implies C(B)⊆C(A).
 cautiously monotonic
 if A⊆B⊆C(A) implies C(A)⊆C(B).
 left logical equivalent
 if ~A↔B implies C(A)=C(B).
 right weakening
 if ~A→B implies ^{1}C({A})⊆^{1}C({B}).
i.e. if ~A→B,C~A implies C~B
 cumulative
 if it is cut and cautiously monotonic.
(thus A⊆B⊆C(A) implies C(B)=C(A)).
 idempotent
 if C(A)=C(C(A)).
 reciprocal
 if A⊆C(B), B⊆C(A) implies C(A)=C(B).
 ...
 if A⊆C({A∨B}) implies C(A)⊆C({A∨B}).
 modus ponens in consequentia
 if F,F→G∈C(A) implies G∈C(A).
 supraclassical
 if A⊢B implies A~B.
 monotonic
 if A⊆B implies C(A)⊆C(B).
⇐ ~ is reflexive and transitive
 transitive
 if A⊆C(B) implies C(A)⊆C(B).
 structural
 if ∀σ∈
SUB
σ(C(A)) ⊆ C(σ(A)))
 compact
 if
B ~ F ⇔ there exists a finite E⊆B with E ~ F
("⇐" if ~ is monotonic)
 uniform
 if,
provided that G and B∪{F} do not have any variables (or (atomic) propositional variables) in common
and G is not inconsistent (i.e. C({G})≠Formula(Σ)),
then
B∪{G} ~ F ⇒ B ~ F
∀A,B⊆Formula(Σ).
By an abuse of language, an inference relation that is reflexive, cut, and cautiously monotonic
is called cumulative inference relation (it satisfies cumulative).
Intersections of cumulative inference relations are cumulative inference relations.
An inference relation satisfies the Csystem if it is a cumulative inference relation
that further supports left logical equivalent and right weakening. There are several implications
within the above properties. For example Csystem inference relation also satisfies (6)(11).
Calculus
Semantic inference relations ≈
are implemented with a syntactic calculus K whose application in relational form
is denoted as ~.
Such a calculus deduces W ~ F,
if F can be deduced with a sequence of inference rules applied on the formulas in W.
A syntactic calculus K should be correlated with the semantic inference relation.
Let V be an alphabet that is provided effectively (f.ex. V=Formula(Σ)),
and L be a language over V, i.e. a decidable set of finite objects over V
(usually words in L=V^{*}).
 inference rule

An nary inference rule is a decidable (n+1)ary relation ρ⊆L^{n+1}.
For an instance (u_{0},...,u_{n1},u_{n})∈ρ,
the u_{0},...,u_{n1} are called premises, and
u_{n} is called the conclusion.
 axiom

Inference rules of arity 0 are called logical axioms since they do not depend on any premises.
 calculus

A calculus K of the language L over V
is a finite set of inference rules in this language L.
Let K be a calculus of the language L over V.
 deduction

A deduction of F∈L from W⊆L is a repeated application of the inference relations of a calculus K.
More formally, a deduction of F∈L from W⊆L is a finite sequence
(u_{1},...,u_{n})⊆L with u_{n}=F such that for all i∈{1,...,n}
 u_{i}∈W is part of the knowledge,
 or there is an inference rule ρ∈K with an arity of n≥0 and there are
j_{1},...,j_{n}∈{1,...,i1} which justify
(u_{j1},...,u_{jn},u_{i})∈ρ.
We then call F deducable from W in K which we denote by the inference relation
W ~ F
Note that this notion of deduction is only a minor generalization (in arity)
of the syntactic deduction in formal languages specified by a Chomsky grammar.
It still can be reduced to the normal case of formal languages.
Let K be a calculus of the language L over V, then the corresponding
inference relation ~ is monotonic, transitive, compact
and
 compositional

W_{i} ~ F_{i} for i=1,...,n, and (F_{1},...,F_{n},F)∈ρ∈K ⇒ ⋃_{i=1,...,n} W_{i} ~ F
These are true due to the above definition of deduction, cf. monotonic inference relations.
The calculus K having a syntactic inference relation ~ is consistent if it is both:
 sound
 if ~ ⊆ ≈,
i.e. all that is deducable is a logical consequence.
 complete
 if ≈ ⊆ ~,
i.e all that is a logical consequence is deducable.
 Author:
 André Platzer
 See Also:
Formula
,
Signature
,
Logic.inference()
,
several inference relations Invariants:
 true
Method Summary 
boolean 
infer(Formula[] w,
Formula d)
Apply the inference relation ~
according to the implementation calculus K. 
boolean 
isComplete()
Whether the calculus K underlying this object to implement the inference relation is complete. 
boolean 
isSound()
Whether the calculus K underlying this object to implement the inference relation is sound. 
infer
boolean infer(Formula[] w,
Formula d)
throws LogicException
 Apply the inference relation ~
according to the implementation calculus K.
 Parameters:
w
 the premises, i.e. basic knowledge formulas assumed true for the inference.
Use an array of length 0
or null
to denote the inference
"∅ ~ w"
from the empty set of knowledge ∅. Only axioms are available then, and thus the result
is equal to that of "true
~ d".
This inference from the empty set is abbreviated as "~ w"
because it will only infer tautologies.d
 the conclusion claimed, i.e. the formula to deduce from w, if possible.
 Returns:
 whether w ~ d, that is whether d can be inferred from the facts in w, or not.
 Throws:
LogicException
 if an exception related to the logic syntax or semantics or the calculus execution occurs. See Also:
 Strategy Pattern
 Preconditions:
 true
 Postconditions:
 ( (RES==true && isSound()) => w ≈ d )
&& ( (w ≈ d && isComplete()) => RES==true )
isSound
boolean isSound()
 Whether the calculus K underlying this object to implement the inference relation is sound.
The calculus K is
 sound
 if ~ ⊆ ≈, i.e. if W ~ F implies W ≈ F.
 Preconditions:
 true
 Postconditions:
 RES == OLD(RES)
isComplete
boolean isComplete()
 Whether the calculus K underlying this object to implement the inference relation is complete.
The calculus K is
 complete
 if ≈ ⊆ ~, i.e. if W ≈ F implies W ~ F.
 Preconditions:
 true
 Postconditions:
 RES == OLD(RES)
Copyright © 19962009 André Platzer
All Rights Reserved.