# 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 * Parsing strings to expressions Read further for examples. ## Types ### Operators There is one unary operator (`Op1`): `Not`. It binds stronger than all other operators. There are four binary operators (`Op2`). In order of descending precedence: `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. The operators are represented as: * Not: `~` * And: `&` * Or: `|` * Impl: `->` * Equiv: `<->` ### 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 ## Parsing The `parse` function may be used to read an expression from a String. The following rules are used: * Whitespace is ignored. * All latin letters (`[a-zA-Z]`) are considered atomic expressions * Operators are expected in their representation described above * True and False are expected as `1` and `0`, respectively A usage example is found in `LogicParser.icl`. This file, once compiled, reads the command line arguments and shows their truth tables: $./LogicParser -b -nt -e "~~(((A | (A -> B)) -> B) -> B)" A | B | A -> B | A | (A -> B) | A | (A -> B) -> B | (A | (A -> B) -> B) -> B | ~((A | (A -> B) -> B) -> B) | ~~((A | (A -> B) -> B) -> B) -------+-------+--------+--------------+-------------------+--------------------------+-----------------------------+------------------------------ False | False | True | True | False | True | False | True False | True | True | True | True | True | False | True True | False | False | True | False | True | False | True True | True | True | True | True | True | False | True Here, `-b` and `-nt` are common Clean options to disable outputting basic values for constructors, and disable outputting execution times, respectively. The option `-e` tells the parser to show the extended truth table. With this option, only the first formula is considered. Without `-e`, multiple formulas may be given (possibly with different atomic expressions), and all will be evaluated in one table: $./LogicParser -b -nt "~~(((A | (A -> B)) -> B) -> B)" "A & B" A | B | ~~((A | (A -> B) -> B) -> B) | A & B -------+-------+------------------------------+------- False | False | True | False False | True | True | False True | False | True | False True | True | True | True False | False | True | False False | True | True | False True | False | True | False 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 * Add support for multi-letter atomic expressions ## License This program and the example are distributed under the MIT license. For more details, see the LICENSE file.