# A Proof Tree Builder for Sequent Calculus and Hoare Logic

arXiv: https://arxiv.org/abs/2303.05865 · HTML: https://mlsanity.com/paper/2303.05865/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Mar 2023.

## Built on by (most cited first, 1 of 1)

- [Teaching Higher-Order Logic Using Isabelle](https://mlsanity.com/paper/2404.05458/) (2024)

## Abstract (arXiv)

We have developed a web-based pedagogical proof assistant, the Proof Tree Builder, that lets you apply rules upwards from the initial goal in sequent calculus and Hoare logic for a simple imperative language. We equipped our tool with a basic proof automation feature and Z3 integration. Students in the automated reasoning course at Princeton University used our tool and found it intuitive. The Proof Tree Builder is available online at https://proof-tree-builder.github.io.