orbital.moon.logic
Class ModalLogic

java.lang.Object
  orbital.moon.logic.ClassicalLogic
      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.
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) in 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 ¬, and , or , ->, for all , exist . 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 , or , ->, <=>, for all and exist .

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. Caution 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.