Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF

Aaron Stump; Clark W Barrett; David L Dill

doi:10.1016/S1571-0661(04)80504-8

Back

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF

Journal article

Open access

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF

Aaron Stump, Clark W Barrett and David L Dill

Electronic notes in theoretical computer science, Vol.70(2), pp.29-41

12/2002

DOI: 10.1016/S1571-0661(04)80504-8

Files and links (1)

url

https://doi.org/10.1016/S1571-0661(04)80504-8View

Published (Version of record) Open Access

Abstract

Software that can produce independently checkable evidence for the correctness of its output has received recent attention for use in certifying compilers and proof-carrying code. CVC (Cooperating Validity Checker) is a proof-producing validity checker for a decidable fragment of first-order logic enriched with background theories. This paper describes how proofs of valid formulas are produced from the decision procedure for linear real arithmetic implemented in CVC. It is shown how extensions to LF which support proof rules schematic in an arity (“elliptical” rules) are very convenient for this purpose.

Details

Title: Subtitle: Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF
Creators: Aaron Stump - Stanford University
Clark W Barrett - Stanford University
David L Dill - Stanford University
Resource Type: Journal article
Publication Details: Electronic notes in theoretical computer science, Vol.70(2), pp.29-41
DOI: 10.1016/S1571-0661(04)80504-8
ISSN: 1571-0661
eISSN: 1571-0661
Publisher: Elsevier B.V
Language: English
Date published: 12/2002
Academic Unit: Computer Science
Record Identifier: 9984259416802771

Metrics

13 Record Views