CleanLogic

Logic toolbox in Clean. Features include:

Straightforward types for (atomic) expressions, operators and truth tables
show (toString-like) 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
A web frontend to access the Clean program through, so only server-side installation is necessary
Different output options (Plain / ASCII art, HTML, LaTeX)

Read further for examples.

Demo

A demo of the web frontend may be found on https://demo.camilstaps.nl/CleanLogic.

License

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

Installation

Set CLEAN_HOME to your Clean installation directory. To install the parser and the example program:

make

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:

Negation (¬): ~
Conjunction (∧): &
Disjunction (∨): |
Implication (→): ->
Equivalence (↔): <->

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 occurrences of Atom a in an Expr e by a Bool b with substitute (a,b) e. This yields a new Expr, in which all occurrences have been replaced by the constant 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:

Spaces are 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
Unknown characters will throw an error

A usage example is found in LogicParser.icl. This file, once compiled, reads the command line arguments and shows their truth tables:

$./LogicParser -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

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

The parsers also recognises -html and -latex and will output an HTML or LaTeX table if these arguments are present.

Web frontend

There is a simple web frontend in PHP and a basic HTML template which allows one to connect to the Clean application through his browser. The files for this are index.html and request.php, and a demo may be found on https://demo.camilstaps.nl/CleanLogic. For this to work, the exec() function should be enabled in your PHP configuration.

Future ideas

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
Would it be easier / neater / more intuitive to get rid of Op1 and Op2 and use Not, And, etc. as type constructors of Expr?