Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

14

JAR
2010

favoriteEmaildiscussreport

160views more JAR 2010»

Declarative Representation of Proof Terms

13 years 3 months ago

Declarative Representation of Proof Terms

Download www.cs.unibo.it

Abstract. We present a declarative language inspired by the pseudonatural 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.

Claudio Sacerdoti Coen

Real-time Traffic

Declarative Language | Declarative Scripts | JAR 2010 | Proof Terms |

claim paper

Related Content

» Procedural Representation of CIC Proof Terms

» A Sequent Calculus with Implicit Term Representation

» Representable Correcting Terms for Possibly Underflowing Floating Point Operations

» Representational Content and the Reciprocal Interplay of Agent and Environment

» An embedded declarative data transformation language

» Syntax for Free Representing Syntax with Binding Using Parametricity

» Kernels on Prolog Proof Trees Statistical Learning in the ILP Setting

» Runtime Addition of Integrity Constraints in an Abductive Proof Procedure

» Declarative Debugging of Missing Answers for Maude

Post Info
More Details (n/a)

Added	28 Jan 2011
Updated	28 Jan 2011
Type	Journal
Year	2010
Where	JAR
Authors	Claudio Sacerdoti Coen

Comments (0)