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 LogicBasisextends java.lang.Objectimplements 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