diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 131 |
1 files changed, 84 insertions, 47 deletions
@@ -3,39 +3,49 @@ 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 + * `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 + * 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. +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. +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: +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 +``` +make +``` ## Types ### Operators -There is one unary operator (`Op1`): `Not`. It binds stronger than all other 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. +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: @@ -47,7 +57,9 @@ The operators are represented as: ### 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`). +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 @@ -77,19 +89,30 @@ Expressions are constants (`B Bool`), atomic expressions (`Atom Char`), or appli ## 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`. +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. +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. +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 `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 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`. @@ -123,50 +146,64 @@ The `truthtable` of `e15`: ## Parsing -The `parse` function may be used to read an expression from a String. The following rules are used: +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 + * 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. +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. +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` + * 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`? + * Would it be easier / neater / more intuitive to get rid of `Op1` and `Op2` + and use `Not`, `And`, etc. as type constructors of `Expr`? |