README.md

# Proof Assistant with Solver
A web-based proof assistant aimed at enhancing the learning of logical proof techniques through Sequent Natural Deduction. Addressing limitations observed in Pandora, our proof assistant integrates advantages from other remarkable systems such as Andy and ProofWeb. The main features include:
- A pure front-end web application for ease of development and accessibility.
- Manual answer entry, rule validation, and "bottom to up" proof construction to encourage deeper understanding of logic.
- An intuitive tree representation for visualizing logical proofs.

This project is implemented by JavaScript and Vue.js. It implemented parser by [Nearley.js](https://nearley.js.org/) and renders the formulas by [KaTeX.js](https://katex.org/), allowing for efficient and accurate parsing and display of logical formulas.


## Project setup

Ensure that Node.js and npm are installed on your system. You can download and install the appropriate version for your operating system from the [Node.js official website](https://nodejs.org/).

In the project directory, run the following command to install the necessary dependencies:
```
npm install
```
This command will download and install all required packages as specified in the package.json file.


## You could try the website

After all dependencies are installed, start the development server to view the project:
```
npm run serve
```
By default, the development server will run on http://localhost:8080. You can open this address in your browser to view this proof assistant.

## User Guide

## Notation
 The following notation was used in our proof assistant. 

 | **Symbol** | **Representation** | **Meaning** |
|------------|--------------------|-------------|
| Not        | `!`                | The negation of a statement. True if the statement is false. |
| And        | `&`                | True if both statements are true. |
| Or         | `\|\|`               | True if at least one of the statements is true. |
| Imply      | `->`               | Indicates implication. True unless the first statement is true and the second is false. |
| Brackets   | `()`               | Used to group statements and indicate precedence. |
| Turnstile  | `\|-`               | Indicates logical entailment or syntactic consequence. |
| True       | `true`             | Represents a true statement. |
| False      | `false`            | Represents a false statement. |
| Symbol     | A single uppercase or lowercase letter | Represents a variable or a constant in logical expressions. |

## Flowchart
**Step 1:** Type a sequent you want to prove in the input line, and click submit.

**Step 2:** Choose the sequent you want to apply the inference rule to by clicking the turnstile.

**Step 3:** There will be a dialog where you could select the inference rule and type your answer and expressions. Click submit for validation.

**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"/>