Producing proofs from an arithmetic decision procedure in elliptical LF

Aaron Stump, Clark W. Barrett, David L. Dill

Research output: Contribution to journalArticle

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.

Original languageEnglish (US)
Pages (from-to)31-43
Number of pages13
JournalElectronic Notes in Theoretical Computer Science
Volume70
Issue number2
DOIs
StatePublished - Dec 2002

Fingerprint

Schematic diagrams
Decision Procedures
First-order Logic
Compiler
Correctness
Fragment
Valid
Software
Output

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Producing proofs from an arithmetic decision procedure in elliptical LF. / Stump, Aaron; Barrett, Clark W.; Dill, David L.

In: Electronic Notes in Theoretical Computer Science, Vol. 70, No. 2, 12.2002, p. 31-43.

Research output: Contribution to journalArticle

Stump, Aaron ; Barrett, Clark W. ; Dill, David L. / Producing proofs from an arithmetic decision procedure in elliptical LF. In: Electronic Notes in Theoretical Computer Science. 2002 ; Vol. 70, No. 2. pp. 31-43.
@article{267a061c1fc84ecc817c9b8e32f92487,
title = "Producing proofs from an arithmetic decision procedure in elliptical LF",
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.",
author = "Aaron Stump and Barrett, {Clark W.} and Dill, {David L.}",
year = "2002",
month = "12",
doi = "10.1016/S1571-0661(04)80504-8",
language = "English (US)",
volume = "70",
pages = "31--43",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - Producing proofs from an arithmetic decision procedure in elliptical LF

AU - Stump, Aaron

AU - Barrett, Clark W.

AU - Dill, David L.

PY - 2002/12

Y1 - 2002/12

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=18944401455&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=18944401455&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)80504-8

DO - 10.1016/S1571-0661(04)80504-8

M3 - Article

AN - SCOPUS:18944401455

VL - 70

SP - 31

EP - 43

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 2

ER -