logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Data.Logic.Classes.Combine

Description

Class Logic defines the basic boolean logic operations, AND, OR, NOT, and so on. Definitions which pertain to both propositional and first order logic are here.

Synopsis

# Documentation

class Negatable formula => Combinable formula whereSource

A type class for logical formulas. Minimal implementation: ``` (.|.) ```

Methods

(.|.) :: formula -> formula -> formulaSource

Disjunction/OR

(.&.) :: formula -> formula -> formulaSource

Derived formula combinators. These could (and should!) be overridden with expressions native to the instance.

| Conjunction/AND

(.<=>.) :: formula -> formula -> formulaSource

Formula combinators: Equivalence

(.=>.) :: formula -> formula -> formulaSource

Implication

(.<=.) :: formula -> formula -> formulaSource

Reverse implication:

(.<~>.) :: formula -> formula -> formulaSource

Exclusive or

(.~|.) :: formula -> formula -> formulaSource

Nor

(.~&.) :: formula -> formula -> formulaSource

Nand

Instances

 Negatable (PropForm a) => Combinable (PropForm a) (Negatable (Formula atom), Ord atom) => Combinable (Formula atom) Negatable (Formula a) => Combinable (Formula a) Negatable (Formula a) => Combinable (Formula a) (Negatable (Sentence v p f), Ord v, Ord p, Ord f) => Combinable (Sentence v p f) (Negatable (Formula v p f), Constants (Formula v p f)) => Combinable (Formula v p f) (Negatable (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Constants (Formula v p f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => Combinable (Formula v p f)

data Combination formula Source

`Combination` is a helper type used in the signatures of the `foldPropositional` and `foldFirstOrder` methods so can represent all the ways that formulas can be combined using boolean logic - negation, logical And, and so forth.

Constructors

 BinOp formula BinOp formula :~: formula

Instances

 Typeable1 Combination Eq formula => Eq (Combination formula) (Typeable (Combination formula), Data formula) => Data (Combination formula) (Eq (Combination formula), Ord formula) => Ord (Combination formula) Read formula => Read (Combination formula) Show formula => Show (Combination formula) SafeCopy formula0 => SafeCopy (Combination formula0) Bijection (Combination (Formula v p f)) (Combination (Formula v p f))

combine :: Combinable formula => Combination formula -> formulaSource

A helper function for building folds: ``` foldPropositional combine atomic ``` is a no-op.

data BinOp Source

Represents the boolean logic binary operations, used in the Combination type above.

Constructors

 :<=>: Equivalence :=>: Implication :&: AND :|: OR

Instances

 Bounded BinOp Enum BinOp Eq BinOp Data BinOp Ord BinOp Read BinOp Show BinOp Typeable BinOp SafeCopy BinOp Pretty BinOp

binop :: Combinable formula => formula -> BinOp -> formula -> formulaSource

# Unicode aliases for Combinable class methods

(∧) :: Combinable formula => formula -> formula -> formulaSource

(∨) :: Combinable formula => formula -> formula -> formulaSource

(⇒) :: Combinable formula => formula -> formula -> formulaSource

⇒ can't be a function when -XUnicodeSyntax is enabled.

(⇔) :: Combinable formula => formula -> formula -> formulaSource

# Use in Harrison's code

(==>) :: Combinable formula => formula -> formula -> formulaSource

(<=>) :: Combinable formula => formula -> formula -> formulaSource