| Description | In formal logic, proofs are formally defined as trees generated from a finite set of rules that typically correspond to informal reasoning steps. This notion is useful as it gives us a way to mathematically model the activity of mathematicians and opened the door to meta-theoretical investigations at the beginning of the 20th century; now the field of proof theory has been active since and the connections with computer science (more specifically, (functional) programming languages, verification and typing) are plentiful.
While concrete proof-trees are seldom used by end users, they still need to be taught and visualized to some extent by theoreticians, though this can be difficult in practice due to size and geometry issues. Nevertheless, there are a few tools that enables to work interactively with such representations for educational purposes like http://logitext.mit.edu/main or https://click-and-collect.linear-logic.org/ for the sequent calculus.
The goal of this project would be to build similar tools for other proof systems, such as natural deduction.
If that sounds too boring, there are also a number of less mainstream proof systems that would deserve their tools. In particular, we could also look at systems with more expansive sets of formulas:
- the μ-calculus (i.e. fixpoint logics)
- modal logic
- second-order quantifications
- linear logic with weak exponential modalities |
|---|