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(Σ)); 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 ^-1C({A})⊆^-1C({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 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 ρ⊆Lⁿ⁺¹. For an instance (u₀,...,u_n-1,u_n)∈ρ, the u₀,...,u_n-1 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₁,...,u_n)⊆L with u_n=F such that for all i∈{1,...,n}

1. u_i∈W is part of the knowledge,
2. or there is an inference rule ρ∈K with an arity of n≥0 and there are j₁,...,j_n∈{1,...,i-1} 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₁,...,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.

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.

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)