Abstract

A sequent calculus of a new sort is extracted from the Prolog program leanTAP. This calculus is sound and complete, even though it lacks almost all structural rules. Thinking of leanTAP as a sequent calculus provides a new perspective on it and, in some ways, makes it easier to understand. It is also easier to verify correctness and completeness of the Prolog implementation. In addition, it suggests extensions to other logics, some of which are considered here.