Proof Assistant is a 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.
Advisor: Prof. John Slaney
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.
The dashboard is where you create new proofs, and also where your existing proofs are listed along with there current status.
The 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.
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.
This is the page where you actually write the proof. All premises of the sequent is auto-populated for you as assumption lines.
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 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.
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.
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. button indicates that the latest proof is saved, while 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".
Enjoy Natural Deductions!