Sciweavers

Share
CADE
1994
Springer

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

9 years 4 months ago
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.
Lars-Henrik Eriksson
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where CADE
Authors Lars-Henrik Eriksson
Comments (0)
books