Skip to content
Online platform to enable Logic students to write, verify, and store System L style Natural Deduction proofs with real-time proof-checking
JavaScript HTML Other
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
FOL
bin
lib/antlr4
models
public
routes
util
views
.bowerrc
.editorconfig
.gitignore
DEPLOYMENT.md
DEVELOPMENT.md
LICENSE.md
README.md
app.js
bower.json
config.js
gulpfile.js
package.json

README.md

Proof Assistant

An online platform to enable Logic students to write, verify, and store System L style Natural Deduction proofs. Proofs are checked for correctness in real-time, and provides informative error messages. The project was developed as part of the Logic4Fun initiative during Logic Summer School, 2015.

Features

  • Real-time and in-browser proof validation
  • Server-side proof validation during save using Isomorphic Javascript
  • Ability to continue writing verified proofs even when the Internet connection is lost
  • User account to save and retrieve proofs
  • Informative error messages
  • Fast and easy way of typing logic statements

Software Stack

  • Javascript
  • Node.js
  • MongoDB
  • ANTLR4
  • Bootstrap
  • Jade

Contributors

Getting Started

Setup an Account

Login/SignUp with any valid email. E-mail is just a placeholder for the username, essentially you can give a random valid email and password as long as you can remember it.

Dashboard

The dashboard is where you create new proofs, and also where your existing proofs are listed along with there current status.

Dashboard The NEW PROOF button brings up a pop-up dialogue where you can enter the sequent you want to prove. Typing the sequent is very easy, the following short-keys auto-convert to their equivalent logical connectives as you type.

  • \n:  ¬ (negation)
  • \a:  ∧ (and)
  • \o:  ∨ (or)
  • \i:  → (implication)
  • \e:  ⊢ (entails)
  • \t:  ⊤ (true)
  • \f:  ⊥ (false)

Example: The sequent "¬(p → q) ⊢ p ∧ ¬q" should be typed as "\n(p \i q) \e p \a \nq". It may look daunting at first, but as you type, it'll becomes natural.

New Proof

Proof Page

This is the page where you actually write the proof. All premises of the sequent is auto-populated for you as assumption lines.

Proof Page

The next proof line is entered using the fields provided at the bottom. The same short-keys mentioned earlier can be used to type in the connectives. Also, it is not necessary to press the + button every time, pressing the enter key on any of the input fields submits your new proof line for validation. If you dont know what these fields are please read the excellent introduction to Propositional Logic and System L style Natural Deduction proofs by Prof. John Slaney.

The platform also provides the ability to delete or edit rows, provided the change does not break the validity of the proof. When a proof line is deleted or edited the proof is not auto-saved on the server. You can see that the SAVE button would be now red in color, indicating an unsaved proof.

Error Messages

Submission of the new proof line triggers validation of the entire proof. Only if the entire proof is valid, the new proof line is added. In case of an invalid proof line, a corresponding error message is displayed.

Error Message

Features

The proof is validated in-browser, i.e. the proof is not sent to the server each time a line is added. This allows fast verification of large proofs and also the ability to use the tool offline. If an internet connection is available, any change made to the proof is auto-saved on the server. The colour of the SAVE button indicates whether the proof was successfully saved on the server or not. A green SAVE button indicates that the latest proof is saved, while a red SAVE button indicates that there are some changes in the proof that are not saved in the server. Note that on each save request the proof is validated on the server-side as well.

When the line that completes the proof is entered, and the proof is validated, the status of the proof changes to SUCCESS.

Success

Enjoy Natural Deductions!

You can’t perform that action at this time.