Validated Proof-Producing Decision Procedures | Zendy

Robert Klapper | Zendy; Aaron Stump | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Validated Proof-Producing Decision Procedures

Author(s) -

Robert Klapper,

Aaron Stump

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2004.06.067

Subject(s) - mathematical proof , computer science , programming language , rewriting , closure (psychology) , debugging , proof assistant , theoretical computer science , automated proof checking , proof complexity , algorithm , automated theorem proving , mathematics , economics , market economy , geometry

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research