Skip to content
Snippets Groups Projects
Commit b3440e18 authored by Jenny Zhang's avatar Jenny Zhang
Browse files

Update Readme document with predefined inference rules of classical logic

parent f96bb725
No related branches found
No related tags found
No related merge requests found
......@@ -29,6 +29,7 @@ By default, the development server will run on http://localhost:8080. You can op
## User Guide
## Notation
The following notation was used in our proof assistant.
| **Symbol** | **Representation** | **Meaning** |
......@@ -43,6 +44,14 @@ By default, the development server will run on http://localhost:8080. You can op
| False | `false` | Represents a false statement. |
| Symbol | A single uppercase or lowercase letter | Represents a variable or a constant in logical expressions. |
## Inference Rules
Our proof assistant incorporates predefined inference rules of classical logic in Sequent Natural Deduction.
The following rules were included in our proof assistant:
<img src="./src/assets/rules1.png" alt="rules1" title="rules1" width="300"/>
<img src="./src/assets/rules2.png" alt="rules2" title="rules2" width="300"/>
## Flowchart
**Step 1:** Type a sequent you want to prove in the input line, and click submit.
......@@ -53,3 +62,4 @@ By default, the development server will run on http://localhost:8080. You can op
**Step 4:** If you are correct, the dialog will disappear, and you could repeat steps 2-3 until you finish your proof.
<img src="./src/assets/userFlowChart.png" alt="User Flowchart" title="User Flowchart" width="300"/>
src/assets/rules1.jpg

219 KiB

src/assets/rules2.jpg

60.1 KiB

0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment