
Orbital library  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
public interface Logic
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:
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:
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.
Signature
,
Formula
,
Interpretation
,
Inference
,
Strategy PatternMethod 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 noncompound 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 

Interpretation coreInterpretation()
This will usually contain the interpretation functors of logical operators like ¬, ∧, ∨, →, ⇔, ∀ and ∃.
ExpressionSyntax.coreSignature()
boolean satisfy(Interpretation I, Formula F)
For multivalued logics, the above definition of a semantic satisfaction relation would experience a small generalization
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.
I
 the interpretation within which to evaluate F.F
 the formula to check whether it is satisfied in I.
IncompleteCalculusException
 if calculus for this logic is not complete.
LogicException
 if an exception related to logic occurs.coreInterpretation()
Inference inference()
IncompleteCalculusException
 if calculus for this logic is not complete.
LogicException
 if an exception related to logic occurs.Expression createAtomic(Symbol symbol) throws java.lang.IllegalArgumentException
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.
createAtomic
in interface ExpressionBuilder
symbol
 the symbol whose atomic expression representation to create.
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.Expression.Composite compose(Expression compositor, Expression[] arg) throws ParseException, TypeException
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
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.
compose
in interface ExpressionBuilder
compositor
 the expression that is used for composing the arguments.arg
 the arguments a
passed to the combining operation.
compositor(a[0],…,a[a.length1])
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.Expression createExpression(java.lang.String expression) throws ParseException, java.lang.IllegalArgumentException
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.
createExpression
in interface ExpressionSyntax
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.
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.

Orbital library 1.3.0: 11 Apr 2009 

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