We present a declarative language inspired by the pseudo-natural language used in Matita for the explanation of proof terms. We show how to compile the language to proof terms and how to automatically generate declarative scripts from proof terms. Then we investigate the relationship between the two translations, identifying the amount of proof structure preserved by compilation and re-generation of declarative scripts.
Declarative Representation of Proof Terms / C. Sacerdoti Coen. - ELETTRONICO. - 07-10:(2007), pp. 3-18. (Intervento presentato al convegno Programming Languages for Mechanized Mathematics Workshop tenutosi a Research Institute for Symbolic Computation, Hagenberg, Austria nel 29-30/06/2007).
Declarative Representation of Proof Terms
SACERDOTI COEN, CLAUDIO
2007
Abstract
We present a declarative language inspired by the pseudo-natural language used in Matita for the explanation of proof terms. We show how to compile the language to proof terms and how to automatically generate declarative scripts from proof terms. Then we investigate the relationship between the two translations, identifying the amount of proof structure preserved by compilation and re-generation of declarative scripts.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
