Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions

Pi is a system for the interactive construction and editing of formal derivations in the calculus of finitary partial inductive definitions. This calculus can be used as a logical framework where object logics are specified, turning Pi into a derivation system for a particular object logic. Noteworthy features of Pi include: a graphic user interface where derivations are presented in tree form, direct manipulation of the derivation tree structure by selection using a mouse, and the ability to edit existing derivations by cutting and pasting as well as by changing the formulae occurring in a derivation. A simple facility for automatic theorem proving has been designed.

• Type: Conference
• Year: 1994
• Where: CADE
• Authors: Lars-Henrik Eriksson
• Keywords: CADE 1994, Formal Derivations, Logical Reasoning, Object Logic, Partial Inductive Definitions