Orbital library

orbital.moon.logic
Class ModalLogic

java.lang.Object
  extended by orbital.moon.logic.ClassicalLogic
      extended by orbital.moon.logic.ModalLogic
All Implemented Interfaces:
Logic, ExpressionBuilder, ExpressionSyntax

public class ModalLogic
extends ClassicalLogic

Implementation of modal logic with local or global consequence.

Author:
André Platzer

Nested Class Summary
 
Nested classes/interfaces inherited from class orbital.moon.logic.ClassicalLogic
ClassicalLogic.InferenceMechanism
 
Field Summary
static java.lang.String usage
           
 
Fields inherited from class orbital.moon.logic.ClassicalLogic
PROPOSITIONAL_INFERENCE, RESOLUTION_HEURISTIC_INFERENCE, RESOLUTION_INFERENCE, RESOLUTION_SATURATION_INFERENCE, SEMANTIC_INFERENCE
 
Constructor Summary
ModalLogic()
           
 
Method Summary
 Formula.Composite composeDelayed(Formula f, Expression[] arguments, Notation notation)
          Delayed composition of a symbol with some arguments.
 Formula.Composite composeFixed(Symbol fsymbol, Functor f, Expression[] arguments)
          Instant composition of functors with a fixed core interperation Usually for predicates etc.
 Interpretation coreInterpretation()
          Get the core interpretation which is fixed for this logic.
 Signature coreSignature()
          Get the core signature which is supported by the language of this expression syntax.
 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.

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.

.
 Formula createFixedSymbol(Symbol symbol, java.lang.Object referent, boolean core)
          Construct (a formula view of) an atomic symbol with a fixed interpretation.
 Formula createSymbol(Symbol symbol)
          Construct (a formula view of) an atomic symbol.
 boolean infer(java.lang.String expression, java.lang.String exprDerived)
          facade for convenience.
 Inference inference()
          Get the inference relation |~K according to the implementation calculus K.
 boolean isLocalConsequence()
          Whether local or global consequence is used.
static void main(java.lang.String[] arg)
          tool-main
protected static boolean proveAll(java.io.Reader rd, orbital.moon.logic.ModernLogic logic, boolean all_true)
          Prove all conjectures read from a reader.
 boolean satisfy(Interpretation I, Formula F)
          Defines the semantic satisfaction relation ⊧.
 Signature scanSignature(java.lang.String expression)
          Scan for the signature Σ of all syntactic symbols in an expression.
 void setLocalConsequence(boolean v)
          Whether to use local or global consequence.
protected  void validateAtomic(Symbol symbol)
          This method validates that a symbol obeys the syntactical conventions imposed by this logic (if any).
 
Methods inherited from class orbital.moon.logic.ClassicalLogic
compose, createAllExpressions, createFormula, createTerm, getInferenceMechanism, setInferenceMechanism, toString
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

usage

public static final java.lang.String usage
See Also:
Constant Field Values
Constructor Detail

ModalLogic

public ModalLogic()
Method Detail

main

public static void main(java.lang.String[] arg)
                 throws java.lang.Exception
tool-main

Throws:
java.lang.Exception

isLocalConsequence

public boolean isLocalConsequence()
Whether local or global consequence is used.


setLocalConsequence

public void setLocalConsequence(boolean v)
Whether to use local or global consequence.

Parameters:
v - true for local consequence, false for global consequence,.

infer

public boolean infer(java.lang.String expression,
                     java.lang.String exprDerived)
              throws ParseException
facade for convenience.

Parameters:
expression - the comma separated list of premise expressions to parse.
Returns:
whether w |~K d.
Throws:
ParseException
See Also:
Facade

satisfy

public boolean satisfy(Interpretation I,
                       Formula F)
Description copied from interface: Logic
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.

Specified by:
satisfy in interface Logic
Overrides:
satisfy in class ClassicalLogic
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.
See Also:
Logic.coreInterpretation()

inference

public Inference inference()
Description copied from interface: Logic
Get the inference relation |~K according to the implementation calculus K.

Specified by:
inference in interface Logic
Overrides:
inference in class ClassicalLogic
Returns:
the inference relation |~K of logical inference.

coreSignature

public Signature coreSignature()
Description copied from interface: ExpressionSyntax
Get the core signature which is supported by the language of this expression syntax.

The core "signature" contains the logical signs that inherently belong to this term algebra and are not subject to interpretation. Logical signs are logical constants like true, false, and logical operators like ¬, ∧, ∨, →, ∀, ∃. The latter are also called logical junctors.

Note that some authors do not count the core "signature" as part of the proper signature Σ but would rather call it "meta"-signature.

Specified by:
coreSignature in interface ExpressionSyntax
Overrides:
coreSignature in class ClassicalLogic
Returns:
the core signature that is valid for every expression following this syntax. Elements in the core signature all have a fixed interpretation.
See Also:
Logic.coreInterpretation()

coreInterpretation

public Interpretation coreInterpretation()
Description copied from interface: Logic
Get the core interpretation which is fixed for this logic.

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

Specified by:
coreInterpretation in interface Logic
Overrides:
coreInterpretation in class ClassicalLogic
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()

proveAll

protected static final boolean proveAll(java.io.Reader rd,
                                        orbital.moon.logic.ModernLogic logic,
                                        boolean all_true)
                                 throws ParseException,
                                        java.io.IOException
Prove all conjectures read from a reader. The conjectures have the following forms
 <premise> (, <premise>)* |= <conclusion>    # <comment> <EOL>
 <formula> == <formula>    # <comment> <EOL>
 ...
 

Parameters:
rd - the source for the conjectures to prove.
logic - the logic to use.
all_true - If true this method will return whether all conjectures in rd could be proven. If false this method will return whether some conjectures in rd could be proven.
Returns:
a value depending upon all_true.
Throws:
ParseException
java.io.IOException
See Also:
LogicParser.readTRS(Reader,ExpressionSyntax,Function)

createAtomic

public Expression createAtomic(Symbol symbol)
Description copied from interface: Logic
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 Logic
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.
See Also:
Factory Method

createSymbol

public Formula createSymbol(Symbol symbol)
Construct (a formula view of) an atomic symbol.

Parameters:
symbol - the symbol for which to create a formula representation
See Also:
ExpressionBuilder.createAtomic(Symbol)

createFixedSymbol

public Formula createFixedSymbol(Symbol symbol,
                                 java.lang.Object referent,
                                 boolean core)
Construct (a formula view of) an atomic symbol with a fixed interpretation.

Parameters:
symbol - the symbol for which to create a formula representation
referent - the fixed interpretation of this symbol
core - whether symbol is in the core such that it does not belong to the proper signature.
See Also:
ExpressionBuilder.createAtomic(Symbol)

composeDelayed

public Formula.Composite composeDelayed(Formula f,
                                        Expression[] arguments,
                                        Notation notation)
Delayed composition of a symbol with some arguments. Usually for user-defined predicates etc. or predicates subject to interpretation.

Parameters:
f - the compositing formula.
arguments - the arguments to the composition by f.
notation - the notation for the composition (usually determined by the composing symbol).

composeFixed

public Formula.Composite composeFixed(Symbol fsymbol,
                                      Functor f,
                                      Expression[] arguments)
Instant composition of functors with a fixed core interperation Usually for predicates etc. subject to fixed core interpretation..

Parameters:
f - the compositing formula.
arguments - the arguments to the composition by f.
fsymbol - the symbol with with the fixed interpretation f.

createExpression

public Expression createExpression(java.lang.String expression)
                            throws ParseException
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.

. Parses single formulas or sequences of formulas delimited by comma and enclosed in curly brackets. Sequences of expressions are represented by a special compound expression encapsulating the array of expressions as its component.

Specified by:
createExpression in interface Logic
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.
See Also:
Factory Method

scanSignature

public Signature scanSignature(java.lang.String expression)
                        throws ParseException
Description copied from interface: ExpressionSyntax
Scan for the signature Σ of all syntactic symbols in an expression.

However, note that this method does not necessarily perform rich type querying. Especially for user-defined functions with an arbitrary argument-type structure, it is generally recommended to construct the relevant signature entries explicitly.

Specified by:
scanSignature in interface ExpressionSyntax
Parameters:
expression - the expression that should be scanned for symbol names.
Returns:
Signature of the syntactic symbols in expression except those of the core signature.
Throws:
ParseException - (optional) when the expression is syntactically malformed. Either due to a lexical or grammatical error. (optional behaviour for performance reasons). Will not throw ParseExceptions if createExpression would not either.
See Also:
ExpressionSyntax.coreSignature(), "Factory Method"

validateAtomic

protected void validateAtomic(Symbol symbol)
                       throws java.lang.IllegalArgumentException
This method validates that a symbol obeys the syntactical conventions imposed by this logic (if any).

Throws:
java.lang.IllegalArgumentException - if signifier is not an identifier.

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.