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
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
|
# 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:
```
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`?
|
