Orbital library

orbital.moon.logic
Class ClassicalLogic

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

public class ClassicalLogic
extends java.lang.Object

Implementation of modern but classical predicate logic (first-order logic).

classical logic
is any logic that accepts tertium non datur (alias the Principle of excluded middle, alias the Principle of bivalence). In a classical logic all logical statements have exactly one truth-value of either true (⊤), or false (⊥). It is a two-valued logic.
non-classical logic
does not assume tertium non datur. Especially, ¬¬φ usually is not equivalent to φ.
What, for example is the truth-value of the following informal statements?
"nowhere in the decimal representation of π does the digit 7 occur 77 times (with the occurrences immediately following each other)"
"Ancient Greeks worshipped Zeus" (cf. free logic)
Most non-classical logics are multi-valued logics.
traditional logic
is the logic prior to Frege
modern logic
is a logic in the spirit of Frege. It provides multiple genericity, which means that multiple quantifiers can concern different individuals. This is possible by using variable symbols.

For the classical logic, the logical deduction relation is called logic sequence (⊨) or semantic sequence. It is a logic inference (correct deduction). Then the inference relation is written as ⊢, the inference operation is called consequence-operation C‍n and the implication is called material classical implication and written as ⇒.

The classical logic is truth-functional and it is:

I(¬A) = true if and only if I(A)=false

For the ClassicalLogic the inference operation is called the consequence operation Cn over ⊨.

Kurt Gödel's Vollständigkeitssatz (1930) proves that there is a sound and complete calculus for first-order logic ⊨ that is semi-decidable. Alonzo Church (1936) and Alan Turing (1936) simultaneously showed that ⊨ is undecidable. (Since the tautological formulas are undecidable, and therefore satisfiable formulas are not even semi-decidable.) The first constructive proof for a sound and complete calculus for ⊨ was due to Alan Robinson (1965).

However, Kurt Gödel's Unvollständigkeitssatz (1931) proves that in first-order logic, the arithmetic theory Theory(N,+,*) is not axiomatizable and thus undecidable. This shows that every sound calculus for an extended first-order logic including arithmetic (N,+,*) and mathematical induction (for N) is incomplete (whatever axioms and inference rules it might have).

Higher-order logic inference rules must be unsound or incomplete anyway. In any case, at least the part of first-order predicate logic without quantifiers, which is called propositional logic, has a simple sound and complete calculus that makes it decidable.

Author:
André Platzer
See Also:
"Gödel, Kurt (1930). Über die Vollstädigkeit des Logikkalküls. PhD Thesis, University of Vienna.", "Gödel, Kurt (1931). Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173-198.", "Church, Alonzo (1936). A note on the Entscheidungsproblem. Journal of Symbolic Logic, 1:40-41 and 101-102.", "Turing, Alan M. (1936). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 2nd series, 42:230-265. Correction published in Vol. 43, pages 544-546."

Nested Class Summary
static class ClassicalLogic.InferenceMechanism
          Specifies the inference mechanism applied for the inference relation.
static class ClassicalLogic.Utilities
          Formula transformation utilities.
 
Field Summary
static ClassicalLogic.InferenceMechanism PROPOSITIONAL_INFERENCE
          Propositional inference.
static ClassicalLogic.InferenceMechanism RESOLUTION_HEURISTIC_INFERENCE
           
static ClassicalLogic.InferenceMechanism RESOLUTION_INFERENCE
          Resolution inference.
static ClassicalLogic.InferenceMechanism RESOLUTION_SATURATION_INFERENCE
           
static ClassicalLogic.InferenceMechanism SEMANTIC_INFERENCE
          Semantic inference with truth-tables.
static java.lang.String usage
           
 
Constructor Summary
ClassicalLogic()
           
ClassicalLogic(ClassicalLogic.InferenceMechanism inferenceMechanism)
          Create a classical logic with the specified inference mechanism.
 
Method Summary
 Expression.Composite compose(Expression compositor, Expression[] arguments)
          Create a compound expression representation with a composition operation.
 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[] createAllExpressions(java.lang.String expressions)
          Create a sequence of (compound) expressions by parsing a list of expressions.
 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 createFormula(java.lang.String expression)
          Deprecated. Use (Formula) createExpression(expression) instead.
 Formula createSymbol(Symbol symbol)
          Construct (a formula view of) an atomic symbol.
 Expression createTerm(java.lang.String expression)
          Parses single term.
protected  ClassicalLogic.InferenceMechanism getInferenceMechanism()
           
 boolean infer(java.lang.String w, java.lang.String d)
          Inference (facade for convenience).
 Inference inference()
          Get the inference relation |~K according to the implementation calculus K.
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 setInferenceMechanism(ClassicalLogic.InferenceMechanism mechanism)
          Set the inference mechanism applied for the inference relation.
 java.lang.String toString()
           
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 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

RESOLUTION_INFERENCE

public static final ClassicalLogic.InferenceMechanism RESOLUTION_INFERENCE
Resolution inference. Inference mechanism driven by full first-order resolution.

Attributes:
computability semi-decidable

RESOLUTION_HEURISTIC_INFERENCE

public static final ClassicalLogic.InferenceMechanism RESOLUTION_HEURISTIC_INFERENCE

RESOLUTION_SATURATION_INFERENCE

public static final ClassicalLogic.InferenceMechanism RESOLUTION_SATURATION_INFERENCE

PROPOSITIONAL_INFERENCE

public static final ClassicalLogic.InferenceMechanism PROPOSITIONAL_INFERENCE
Propositional inference. Inference mechanism specialized for fast propositional inference. Currently uses Davis-Putnam-Loveland algorithm.

Attributes:
time complexity CoNP-complete

SEMANTIC_INFERENCE

public static final ClassicalLogic.InferenceMechanism SEMANTIC_INFERENCE
Semantic inference with truth-tables.

This inference mechanism is usually slow, but has the advantage of involving no calculus but directly following the semantics of formulas. Inspite of its bad average performance, it may be superior to other propositional inference mechanisms in pathological cases or cases with a very small number of different propositional atoms and large formulas.

Constructor Detail

ClassicalLogic

public ClassicalLogic()

ClassicalLogic

public ClassicalLogic(ClassicalLogic.InferenceMechanism inferenceMechanism)
Create a classical logic with the specified inference mechanism.

Parameters:
inferenceMechanism - the inference mechanism applied for the inference relation.
See Also:
setInferenceMechanism(InferenceMechanism)
Method Detail

main

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

Throws:
java.lang.Exception

toString

public java.lang.String toString()

setInferenceMechanism

public void setInferenceMechanism(ClassicalLogic.InferenceMechanism mechanism)
Set the inference mechanism applied for the inference relation.

See Also:
inference(), SEMANTIC_INFERENCE, RESOLUTION_INFERENCE

getInferenceMechanism

protected ClassicalLogic.InferenceMechanism getInferenceMechanism()

createTerm

public Expression createTerm(java.lang.String expression)
                      throws ParseException
Parses single term.

Throws:
ParseException
See Also:
createExpression(String)

compose

public Expression.Composite compose(Expression compositor,
                                    Expression[] arguments)
                             throws ParseException
Description copied from interface: Logic
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 Logic
Specified by:
compose in interface ExpressionBuilder
Parameters:
compositor - the expression that is used for composing the arguments.
arguments - 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).
See Also:
Factory Method

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.

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.

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.

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

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()

createAllExpressions

public Expression[] createAllExpressions(java.lang.String expressions)
                                  throws ParseException
Create a sequence of (compound) expressions by parsing a list of expressions. This method is like createExpression(String), but restricted to lists of expressions.

For example, in the context of conjectures when given

 {A&B, A&~C}
 
an implementation could parse it as two formulas A&B and A&~C.

Parameters:
expressions - the comma separated list of expressions to parse.
Throws:
ParseException
See Also:
Convenience Method, createExpression(String)

createFormula

public Formula createFormula(java.lang.String expression)
                      throws ParseException
Deprecated. Use (Formula) createExpression(expression) instead.

Convenience method.

Throws:
ParseException
See Also:
Convenience method

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"

infer

public boolean infer(java.lang.String w,
                     java.lang.String d)
              throws ParseException
Inference (facade for convenience).

Parameters:
w - the comma separated list of premise expressions to parse.
Returns:
whether w |~K d.
Throws:
ParseException
See Also:
Facade Method, Convenience Method, createAllExpressions(String), createExpression(String), Inference.infer(Formula[],Formula)

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.