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

See Also:

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.