The idea is to provide a simple checker for basic logic proofs that students generate in the sort of discrete math/logic course that is often required in Computer Science programs. In these courses, students often struggle with the basic question of "is this correct?" in ways that don't come up in an intro programming course because there the compiler/interpreter gives them hard feedback. So while students in an intro programming course are forced to face confusion about things like syntax right away, in our logic/discrete course students can flail on basic syntactic issues for weeks, and are often very frustrated because they just don't know if "they've done it right".
This project is a web-based ClojureScript tool that will allow students to check the correctness of each step in their proofs, at least for simple propositional calculus. The basic functionality is in place, but there is a lot of work to be done before this will be a tool that students will want to use for checking more than a few steps of a proof.
See the dev guide for more info about how the project is set up.
Clone and run this repository to see the app in action
git clone https://github.com/UMM-CSci/edsger.git
cd edsger
lein figwheel
See this page for instructions on making figwheel work with Spacemacs.
npm install
PATH="$(pwd)/node_modules/karma-cli/bin:$PATH"
lein doo chrome test once
These steps assume you have Chrome. If want to run the tests in Firefox, simply
replace chrome with firefox.
Tips:
- If you omit
oncefrom the end of the command, the tests be re-run every time that Karma detects a change in the compiled JS files. Very handy when developing tests. - Check out direnv if you want to avoid manually setting your
PATH. - If you wish to avoid opening a browser window
for the tests, use
chrome-headlessinstead (requires Chrome 59 or later).
Users enter a starting expression, a rule they wish to use, and the ending expression. To cite a rule, the rule must be given in two pieces: a left-hand rule that matches the expression we are starting from, and a right-hand rule that matches the expression we end up with.
So, when you validate a logic expression looking like:
a ∧ (c ∨ b)
≣ <(3.24) Symmetry of ∨>
a ∧ (b ∨ c)
you need to type the expressions and rules similar to the above expression.
top-expression box: | a ∧ (b ∨ c) |
left-rule box: | p ∨ q | ≣ | q ∨ p | :right-rule box
bottom-expression box : | a ∧ (c ∨ b) |
≣ or ∨, you don't have to copy them
from somewhere. edsger is doing conversion for you when you type Java-like symbols.
Below is the conversion table.
| Logic Symbol | Regular Symbol (on keyboard) |
|---|---|
| ¬ (not) | ! or "not" |
| ∧ (and) | &, ^, or "and" |
| ∨ (or) | | or "or" |
| ⇒ (implication) | =>, ->, or "implies" |
| ≡ (equivalence) | == or "equiv" |
Click the + button to add steps to your proof, and the - button if you accidentally add too many. edsger will not run if any input box is empty.
Finally, click the validate button to check your reasoning 💯.
The logic symbols given in the table above are the only ones that we currently
support. The parser has knowledge of precedence, but series of operators with
equal precendence need to be made unambigious with parens. We see this in the
example above, but another example would be a ∧ b ∧ c, which would not parse
unless you add parens to make either (a ∧ b) ∧ c or a ∧ (b ∧ c).
Distributed under the Eclipse Public License version 2.0.