Orbital library

## 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 non-logical 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(Σ)); WC(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 AC(A).
cut
if ABC(A) implies C(B)⊆C(A).
cautiously monotonic
if ABC(A) implies C(A)⊆C(B).
left logical equivalent
if |~AB implies C(A)=C(B).
right weakening
if |~AB implies -1C({A})⊆-1C({B}).
i.e. if |~AB,C|~A implies C|~B
cumulative
if it is cut and cautiously monotonic.
(thus ABC(A) implies C(B)=C(A)).
idempotent
if C(A)=C(C(A)).
reciprocal
if AC(B), BC(A) implies C(A)=C(B).
...
if AC({AB}) implies C(A)⊆C({AB}).
modus ponens in consequentia
if F,FGC(A) implies GC(A).
supraclassical
if AB implies A|~B.
monotonic
if AB implies C(A)⊆C(B).
|~ is reflexive and transitive
transitive
if AC(B) implies C(A)⊆C(B).
structural
if ∀σ∈`SUB` σ(C(A)) ⊆ C(σ(A)))
compact
if
B |~ F ⇔ there exists a finite EB 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 C-system 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 C-system 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 n-ary inference rule is a decidable (n+1)-ary relation ρ⊆Ln+1. For an instance (u0,...,un-1,un)∈ρ, the u0,...,un-1 are called premises, and un 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 (u1,...,un)⊆L with un=F such that for all i∈{1,...,n}
1. uiW is part of the knowledge,
2. or there is an inference rule ρ∈K with an arity of n≥0 and there are j1,...,jn∈{1,...,i-1} which justify (uj1,...,ujn,ui)∈ρ.
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
Wi |~ Fi for i=1,...,n, and (F1,...,Fn,F)∈ρ∈K ⇒ ⋃i=1,...,n Wi |~ 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
`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.

Method Detail

### 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.
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)

Orbital library
1.3.0: 11 Apr 2009