Orbital library

orbital.logic.imp
Class LogicBasis

java.lang.Object
  extended by 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

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.

Orbital library
1.3.0: 11 Apr 2009

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