1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
# CleanLogic
Logic toolbox in [Clean](http://wiki.clean.cs.ru.nl/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:
clm -I $CLEAN_HOME/lib/StdLib -I $CLEAN_HOME/lib/ArgEnv LogicParser -o LogicParser
clm -I $CLEAN_HOME/lib/StdLib -I $CLEAN_HOME/lib/ArgEnv LogicTest -o LogicTest
## 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 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:
* 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 -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
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`?
|
