Paper Info
Title
Trusted Theorem Proving: A Case Study in SLD-Resolution
Abstract
Prolog's implementation of SLD-resolution furnishes ail efficient theorem-proving technique, for the Horn-clause subset of first-order logic, and makes for a powerful addition to any automatic or semiautomatic verification system. However, due to the complexity of SLD-resolution. a naive incorporation of a Prolog engine into such a system would inordinately increase the overall trusted base. In this paper We show how to integrate this procedure in a disciplined, trusted manner, by making the Prolog engine justify its results with very simple natural deduction reasoning. In effect, instead of taking SLD-resolution as a primitive inference rule, we, express it, as a derived inference rule in terms of much simpler rules such as conditional elimination. This reduction is an example of a general methodology for building highly reliable soft,ware systems called certified computation, whereby a program not only produces a result r for a given input x but also proves that r is correct for x. Such a proof call be viewed as, a certificate for the result v, and call significantly enhance the latter's credibility: if we trust the axioms and inference rules used ill the proof, we can trust the result. We present a complete implementation of a certifying Prolog interpreter that relies; only oil three exceptionally simple inference rules: conditional elimination. universal specialization, and conjunction introduction.
Year
DOI
Venue
2008
10.1007/978-3-540-88479-8_56
Communications in Computer and Information Science
Keywords
Field
DocType
theorem proving,natural deduction,first order logic,inference rule
SLD resolution,Deduction theorem,Programming language,Horn clause,Computer science,Sequent calculus,Algorithm,Prolog,Resolution (logic),Rule of inference,Formal proof
Conference
Volume
ISSN
Citations 
17
1865-0929
0
PageRank 
References 
Authors
0.34
8
2
Name
Order
Citations
PageRank
Konstantine Arkoudas118619.63
Olin Shivers229430.14