Producing proofs from an arithmetic decision procedure in elliptical LF

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

Research output: Contribution to journalConference articlepeer-review

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)29-41
Number of pages13
JournalElectronic Notes in Theoretical Computer Science
Volume70
Issue number2
DOIs
StatePublished - Dec 2002
EventLFM 2002 International Workshop on Logical Frameworks and Meta-Languages (FLoC Satellite Event) - Copenhagen, Denmark
Duration: Jul 26 2002Jul 26 2002

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Producing proofs from an arithmetic decision procedure in elliptical LF'. Together they form a unique fingerprint.

Cite this