Validated Proof-Producing Decision Procedures

Robert Klapper; Aaron Stump

doi:10.1016/j.entcs.2004.06.067

Back

Validated Proof-Producing Decision Procedures

Journal article

Open access

Validated Proof-Producing Decision Procedures

Robert Klapper and Aaron Stump

Electronic notes in theoretical computer science, Vol.125(3), pp.53-68

07/18/2005

DOI: 10.1016/j.entcs.2004.06.067

Files and links (1)

url

https://doi.org/10.1016/j.entcs.2004.06.067View

Published (Version of record) Open Access

Abstract

A widely used technique to integrate decision procedures (DPs) with other systems is to have the DPs emit proofs of the formulas they report valid. One problem that arises is debugging the proof-producing code; it is very easy in standard programming languages to write code which produces an incorrect proof. This paper demonstrates how proof-producing DPs may be implemented in a programming language, called Rogue-Sigma-Pi (RSP), whose type system ensures that proofs are manipulated correctly. RSP combines the Rogue rewriting language and the Edinburgh Logical Framework (LF). Type-correct RSP programs are partially correct: essentially, any putative LF proof object produced by a type-correct RSP program is guaranteed to type check in LF. The paper describes a simple proof-producing combination of propositional satisfiability checking and congruence closure implemented in RSP.

Congruence Closure

Decision Procedure

Logical Framework

Proof Production

Details

Title: Subtitle: Validated Proof-Producing Decision Procedures
Creators: Robert Klapper - Washington University in St. Louis
Aaron Stump - Washington University in St. Louis
Resource Type: Journal article
Publication Details: Electronic notes in theoretical computer science, Vol.125(3), pp.53-68
DOI: 10.1016/j.entcs.2004.06.067
ISSN: 1571-0661
eISSN: 1571-0661
Publisher: Elsevier B.V
Language: English
Date published: 07/18/2005
Academic Unit: Computer Science
Record Identifier: 9984259466902771

Metrics

11 Record Views