# CleanLogic

Logic toolbox in [Clean](http://wiki.clean.cs.ru.nl/Clean). Features include:

 * Straightforward types for (atomic) expressions, operators and truth tables
 * `toString` instances for all types that take care of associativity
 * Substituting atomic expressions for constants
 * Evaluating expressions without atomic expressions
 * Generating truth tables for expressions, possibly with intermediate steps
 * Displaying truth tables

Read further for examples.

## Types

### Operators

There is one unary operator (`Op1`): `Not`. 

There are four binary operators (`Op2`): `And`, `Or`, `Impl` and `Equiv`. `And` is considered left-associative; all others are considered right-associative. Associativity is only important in `toString` functions. `Expr` itself is an unambiguous recursive type.

### Expressions

Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or applications of operators on other expressions (`App1 Op1 Expr` or `App2 Expr Op2 Expr`).

### Examples

    // Some random examples
    e1 = Atom 'p'
    e2 = Atom 'q'
    e3 = App1 Not e1
    e4 = App2 e1 And e2
    e5 = App2 e3 Or e2
    e6 = App2 e3 Impl e3
    e7 = App2 e4 Equiv e5
    e8 = App2 (App2 (Atom 'p') And (Atom 'q')) Impl (Atom 'q')
    e9 = App2 (Atom 'p') And (App2 (Atom 'q') Impl (Atom 'q'))
    
    // To test associativity rules
    e10 = App2 (App2 (Atom 'p') And (Atom 'q')) And (Atom 'r')
    e11 = App2 (Atom 'p') And (App2 (Atom 'q') And (Atom 'r'))
    
    e12 = App2 (App2 (Atom 'p') Or (Atom 'q')) Or (Atom 'r')
    e13 = App2 (Atom 'p') Or (App2 (Atom 'q') Or (Atom 'r'))
    
    e14 = App2 (App2 (Atom 'p') Impl (Atom 'q')) Impl (Atom 'r')
    e15 = App2 (Atom 'p') Impl (App2 (Atom 'q') Impl (Atom 'r'))
    
    e16 = App2 (App2 (Atom 'p') Equiv (Atom 'q')) Equiv (Atom 'r')
    e17 = App2 (Atom 'p') Equiv (App2 (Atom 'q') Equiv (Atom 'r'))

## Substitution

You can substitute all occurences of `Atom a` in an `Expr e` by a `Bool b` with `substitute (a,b) e`. This yields a new `Expr`, in which all occurences have been replaced by the contstant `B b`.

An alternative is `substitute_all`, which takes a list of tuples `(a :: AtomName, b :: Bool)` and substitutes all atomnames with the corresponding booleans.

## Evaluation

An expression `e` **without atomic expressions** may be evaluated to its result by calling `eval e`. This yields the empty list `[]` if `e` *did* have atomic expressions, or a singleton `[b :: Bool]` with the result of the evaluation.

## Truth tables

A `TruthTable` has a list of expressions `exprs` and a list of `options`, which has the type `[[(AtomName,Bool)]]` and describes all the options the truth table should list.

A simple truth table of an expression `e` contains only the atomic expressions in `e` and `e` itself. It may be built with `simple_truthtable e`. A more complex truth table lists all `e`'s subexpressions. In either table, the expressions are roughly sorted by complexity.

A truth table `table` can be shown with `toString table`.

### Examples

The `simple_truthtable` of `e10`:

     p     | q     | r     | p & q & r 
    -------+-------+-------+-----------
     False | False | False | False     
     False | False | True  | False     
     False | True  | False | False     
     False | True  | True  | False     
     True  | False | False | False     
     True  | False | True  | False     
     True  | True  | False | False     
     True  | True  | True  | True      

The `truthtable` of `e15`:

     p     | q     | r     | q -> r | p -> q -> r 
    -------+-------+-------+--------+-------------
     False | False | False | True   | True        
     False | False | True  | True   | True        
     False | True  | False | False  | True        
     False | True  | True  | True   | True        
     True  | False | False | True   | True        
     True  | False | True  | True   | True        
     True  | True  | False | False  | False       
     True  | True  | True  | True   | True        

## Future ideas

 * Different `toString` formats for operators: HTML (`¬`), UTF-8 (¬), LaTeX (`\neg`)
 * Different `toString` formats for booleans: `0` and `1` or `T` and `F` instead of `True` and `False`
 * Simplifying expressions with atomic expressions as far as possible
 * Testing equivalence or impliance of expressions with atomic expressions

## License

This program and the example are distributed under the MIT license. For more details, see the LICENSE file.