Sequent Calculus Prover

Updated version of Dr Brandon Bennett's Sequent Calculus Prover base on his Google Collab

Basic updates...

• Includes rewriting sequents of the form $P\to Q$ to be $\neg P \lor Q$
• Creates an output file, markdown and KaTeX format, in a hierarchical (list) structure
• Added a method to accept strings of native format e.g. md=sq.prove_from_string('¬(𝑝∧𝑞)⇒(¬𝑝∨¬𝑞)' that returns markdown
• Includes a Jupyter notebook to demonstrate a few proofs

Example Usage

from sequent_calculus_prover import SequentCalculus
sq = SequentCalculus()
sq.prove({('-',('p','&',('-','q')))},{('p','>','q')})
sq.write_to_file('example-proof.md')

And

from sequent_calculus_prover import SequentCalculus
from IPython.display import Markdown, display

default = '((P∨Q)∨R),(¬P∨S),¬(Q∧¬S)⇒(R∨S)'
user_sequent = input(f"Enter value [{default}]: ")
if user_sequent.strip() == "":
    user_sequent = default

sq = SequentCalculus()
markdown_seq_proof=sq.prove_from_string(user_sequent)
display(Markdown(markdown_seq_proof))

The created file can be viewed in many markdown readers showing the full logical symbols.

Improvements needed

• would be great to have a better way to visualise the "split" sequents, when an expression gets divided in two so they're on the same level