orbital.logic.imp
Interface Logic

All Superinterfaces:

ExpressionBuilder, ExpressionSyntax

All Known Implementing Classes:

ClassicalLogic, FuzzyLogic, ModalLogic

public interface Logic
extends ExpressionSyntax

Provides a unified encapsulation of logical systems. This interface encapsulates access to the logic inference relations and satisfaction relations defined for a logical system.

All subsequent logics define these relations for inference and reasoning:

• satisfaction relation: I ⊧ F.
• inference relation: W |~ F.

for a formula F over Σ, a set W of formulas, and an interpretation I of the signature Σ of a language L=Formula(Σ). For a logic, syntax of the representation and semantics for the world must be exactly defined. A general logic consists of:

1 Syntax

Signature:

A signature Σ is the set of the syntactic symbols applicable for objects. Those are symbolic names for constants, functions/arity, variables, predicates/arity, objects, properties of objects, relations between objects.

Formulas:

A Σ-formula F∈Formula(Σ) over a signature Σ is an element of all possible, well-formed formulas that can be build with this signature. The set of well-formed formulas is a formal language over the alphabet Σ as defined in the super class. Formulas define the syntax for the representation of statements concerning the world. They are recursively build with atoms (of the signature) that are combined with functors: junctors ⋆ and quantifiers @.
Common basic junctors are logic junction operations like, for example, the binary conjunction and (short ∧), the binary disjunction or (short ∨) and the unary negation not (short ¬). Quantifiers are logic operations like, for example, the existence quantifier (short ∃) and the all-quantifier (short ∀).

2 Semantics

Interpretations:

A Σ-interpretation I∈Int(Σ) of a signature Σ is the association of the syntactic symbols in Σ with the semantic elements in the world. Such elements are objects of the universe, functions within the model world and relations in it. Only the interpretation gives a semantic meaning to the arbitrary names of the signature.

Satisfaction Relations:

A (semantic) satisfaction relation ⊧ ⊆ Int(Σ)×Formula(Σ) of a signature Σ is the connection between syntactic representation with formulas and their semantic interpretations for the world. I ⊧ F says whether a (compound) formula F is valid in an interpretation I.

Pragmatics comes into play when we consider the consequences of interpreting formulas in the semantics of the specific application at hand. For a logic, one or more inference relations between existing knowledge and derived knowledge can be defined. Logic systems can formally be classified with the characteristics of their inference relations.

One important semantic inference relation is the logic sequence (or entailment) between formulas which is again denoted as ⊨. It can easily be adapted from the satisfaction relation. Then for W ⊨ F all those interpretations I that satisfy the Formulas in W are considered:

• If sceptic inference is applied, I ⊧ F must be true for all Interpretations I that satisfy W.
  For sets of formulas this is defined as: FM ⊨ GM iff Mod_Σ(FM)⊆Mod_Σ(GM) This is the usual case.
• If credulous inference is applied, I ⊧ F must match for at least one Interpretation I that satisfies W.

Now we can define logical equivalence of formulas with the logic sequence.

logical equivalence

≡ ⊆ Formula(Σ)×Formula(Σ) with A≡B :⇔ ⊨ A↔B ⇔ for all interpretations I (with variable assignements) I(A) = I(B) ⇔ A ⊨ B and B ⊨ A

Note:

The last equivalence is only true provided that we do not use global entailment but local entailment.

Other inference relations |~ can be defined with the logic sequence ⊨. Depending upon the inferential problem and whether the formulas are incomplete and which should be inferred, several inference relations are possible.

Note that it is generally undefined to use formulas of one logic within another logic. It may be possible, though, in some special cases of compatible logics.

Author:

André Platzer

See Also:

Signature, Formula, Interpretation, Inference, Strategy Pattern

Invariants:

true

Structure:

extends ExpressionSyntax

Method Summary

Expression.Composite	compose(Expression compositor, Expression[] arg) Create a compound expression representation with a composition operation.
Interpretation	coreInterpretation() Get the core interpretation which is fixed for this logic.
Expression	createAtomic(Symbol symbol) Create an atomic expression representation of a non-compound sign.
Expression	createExpression(java.lang.String expression) Create a term representation by parsing a (compound) expression.
Inference	inference() Get the inference relation |~K according to the implementation calculus K.
boolean	satisfy(Interpretation I, Formula F) Defines the semantic satisfaction relation ⊧.

Methods inherited from interface orbital.logic.sign.ExpressionSyntax

coreSignature, scanSignature

Method Detail

coreInterpretation

Interpretation coreInterpretation()

Get the core interpretation which is fixed for this logic.

This will usually contain the interpretation functors of logical operators like ¬, ∧, ∨, →, ⇔, ∀ and ∃.

Returns:

the core interpretation that is valid for every expression, for fixed interpretation semantics. Elements in the core signature all have a fixed interpretation.

See Also:

ExpressionSyntax.coreSignature()

Preconditions:

true

Postconditions:

RES == OLD(RES) ∧ RES unmodifiable ∧ RES.getSignature() == coreSignature()

satisfy

boolean satisfy(Interpretation I,
                Formula F)

Defines the semantic satisfaction relation ⊧. I ⊧ F, which is usually iff I(F) = true In other words, returns whether I is a satisfying Σ-Model of F.

For multi-valued logics, the above definition of a semantic satisfaction relation would experience a small generalization

I ⊧ F, iff I(F) ∈ D for a fixed set D of designated truth-values.

Unlike the implementation method Formula.apply(Object), this surface method must automatically consider the core interpretation of this logic for symbol interpretations (and possible redefinitions) as well.

Parameters:

I - the interpretation within which to evaluate F.

F - the formula to check whether it is satisfied in I.

Returns:

whether I ⊧ F, i.e. whether I satisfies F.

Throws:

IncompleteCalculusException - if calculus for this logic is not complete.

LogicException - if an exception related to logic occurs.

See Also:

coreInterpretation()

Preconditions:

F∈L(F.getSignature()) "F is a formula in this logic"

inference

Inference inference()

Get the inference relation |~_K according to the implementation calculus K.

Returns:

the inference relation |~_K of logical inference.

Throws:

IncompleteCalculusException - if calculus for this logic is not complete.

LogicException - if an exception related to logic occurs.

createAtomic

Expression createAtomic(Symbol symbol)
                        throws java.lang.IllegalArgumentException

Create an atomic expression representation of a non-compound sign.

Atomic symbols are either elemental atoms, strings or numbers. ☡ In contrast, a logical formula that is not compound of something (on the level of logical junctors) like "P(x,y)" is sometimes called atom.

Note

A compound expression like "P(x)" will not be atomic symbols (although a logic might consider such single predicate applications as atomic in the sense of atomicity on the level of logical junctors). However, the variable "x", and the predicate symbol "P" are atomic symbols.

Specified by:

createAtomic in interface ExpressionBuilder

Parameters:

symbol - the symbol whose atomic expression representation to create.

Returns:

an instance of Expression that represents the atomic symbol in this logic.

Throws:

java.lang.IllegalArgumentException - if the symbol is illegal for some reasons. Note that this is a rather rare case and no parsing is involved at all, which is why this method does not throw a ParseException.

See Also:

Factory Method

Postconditions:

RES instanceof Formula

compose

Expression.Composite compose(Expression compositor,
                             Expression[] arg)
                             throws ParseException,
                                    TypeException

Create a compound expression representation with a composition operation. Connects expressions with a compositor to form a complex expression.

Signature.get(String,Object[]) may be useful for determining the right functor symbol for a composition in case of an atomic compositor.

☡ Be aware that this method does a composition (in the sense of semiotics) of signs/expressions, but not usually a composition (in the sense of mathematics) of functions. Mathematically speaking, the composition that this method performs would usually be called application instead of composition. Although composition (in the sense of mathematics) and application are correlated, they have different types at first sight

∘:(σ→τ)×(τ'→σ') → (τ→τ'); (g,f) ↦ g∘f = (x↦g(f(x))), provided that σ' ≤ σ

_(_):(σ→τ)×σ' → τ; (f,x) ↦ f(x) provided that σ' ≤ σ

Yet together with λ-abstraction, composition can be expressed in terms of application (as the definition above shows). And in conjunction with the (selective) identification of type void→σ' with σ' application can also be expressed per composition.

Specified by:

compose in interface ExpressionBuilder

Parameters:

compositor - the expression that is used for composing the arguments.

arg - the arguments a passed to the combining operation.

Returns:

an expression that represents the combined operation with its arguments, like in

compositor(a[0],…,a[a.length-1])

Throws:

ParseException - if the composition expression is syntactically malformed. Either due to a lexical or grammatical error (also due to wrong type of arguments).

TypeException - if the arguments have the wrong type for composition, i.e. compositor.getType().on(typeOf(arg)) raises a TypeException. Note that type errors are still a kind of syntactic errors, but should be separated from pure parse exceptions in order to simplify distinction for exception handlers.

See Also:

Factory Method

Postconditions:

RES instanceof Formula.Composite

createExpression

Expression createExpression(java.lang.String expression)
                            throws ParseException,
                                   java.lang.IllegalArgumentException

Create a term representation by parsing a (compound) expression.

In fact, parsing expressions is only possible with a concrete syntax. So implementations of this method are encouraged to define and parse a standard notation which can often be close to the default notation of the abstract syntax.

Specified by:

createExpression in interface ExpressionSyntax

Parameters:

expression - the compound expression to parse. A string of "" denotes the empty expression. However note that the empty expression may not be accepted in some term algebras. Those parsers rejecting the empty expression are then inclined to throw a ParseException, instead.

Returns:

an instance of Expression that represents the given expression string in this language.

Throws:

ParseException - when the expression is syntactically malformed. Either due to a lexical or grammatical error.

java.lang.IllegalArgumentException - if the symbol is illegal for some reasons. This may occur like in ExpressionBuilder.createAtomic(Symbol), and due to the same reasons. However, most of the causes (like f.ex. spaces in the signifier) cannot occur here anyway, except when the parser underlying this method's implementation had errors.

See Also:

Factory Method

Preconditions:

expression≠""

Postconditions:

RES instanceof Formula