Orbital library

orbital.logic.imp Class LogicBasis

java.lang.Object orbital.logic.imp.LogicBasis
All Implemented Interfaces:
Function, Functor, Formula, Expression, Typed

public abstract class LogicBasis
extends java.lang.Object
implements Formula

This abstract LogicBasis class derives the extended logic operations depending upon basic logic operations.

Extended logic operations are emulated with the simpler logic operations. Then only the simpler operations must be implemented for a logic. This is not valid for all Logics, but for ClassicalLogic and derivatives.

All formulas of classical logic can be transformed into formulas with a reduced subset of logical operators applied. This is due to the fact that some logical operators themselves can be written with a smaller subset of operators. Some operator systems sufficient for classical first-order predicate logic are

• (∧, ∨, ¬, true, false, ∀)
• (∧, ∨, ¬, ∀)
• (∧, ¬, ∀)
• (∨, ¬, ∀)
• (→, false, ∀)
• (→, ¬, ∀) the Frege logic
• (, ∀) with nand-operator a b = a ∧ b = ¬(a ∧ b).
• (, ∀) with nor-operator a b = a ∨ b = ¬(a ∨ b).

Author:
André Platzer
ClassicalLogic

Nested Class Summary

Nested classes/interfaces inherited from interface orbital.logic.imp.Formula
Formula.Composite

Nested classes/interfaces inherited from interface orbital.logic.functor.Functor
Functor.Specification

Field Summary

Fields inherited from interface orbital.logic.functor.Function
callTypeDeclaration

Constructor Summary
LogicBasis()

Method Summary
Formula equiv(Formula B)
Equivalence equiv: A ⇔ B is calced (A→B) ∧ (B→A)
Formula exists(Symbol x)
Existence-quantifier exists: x A is calced ¬∀x ¬A.
Formula forall(Symbol x)
All-quantifier forall: x A is calced ¬∃x ¬A.
Formula impl(Formula B)
Implication impl: A → B is calced ¬A ∨ B
Formula xor(Formula B)
Exclusion xor: A xor B is calced (A∧¬B) ∨ (¬A∧B)

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface orbital.logic.imp.Formula
and, apply, equals, getBoundVariables, getFreeVariables, getVariables, hashCode, not, or

Methods inherited from interface orbital.logic.sign.Expression
getSignature

Methods inherited from interface orbital.logic.sign.type.Typed
getType

Methods inherited from interface orbital.logic.functor.Functor
toString

Constructor Detail

LogicBasis

public LogicBasis()
Method Detail

xor

public Formula xor(Formula B)
Exclusion xor: A xor B is calced (A∧¬B) ∨ (¬A∧B)

Specified by:
xor in interface Formula

impl

public Formula impl(Formula B)
Implication impl: A → B is calced ¬A ∨ B

Specified by:
impl in interface Formula

equiv

public Formula equiv(Formula B)
Equivalence equiv: A ⇔ B is calced (A→B) ∧ (B→A)

Specified by:
equiv in interface Formula

forall

public Formula forall(Symbol x)
All-quantifier forall: x A is calced ¬∃x ¬A. x for all elements of the world.

Should be overwritten to throw UnsupportedOperationException if neither forall nor exists are supported.

Specified by:
forall in interface Formula
Parameters:
x - is a symbol x for all elements of the world.

exists

public Formula exists(Symbol x)
Existence-quantifier exists: x A is calced ¬∀x ¬A. x is an element of the world.

Should be overwritten to throw UnsupportedOperationException if neither forall nor exists are supported.

Specified by:
exists in interface Formula
Parameters:
x - is a symbol x for an element of the world.

Orbital library
1.3.0: 11 Apr 2009