Incomplete Proofs and Program Synthesis

G. Mints

The theory of deductive program synthesis and verification relies on complete proofs of specifications. Such proofs are assumed to be found by an automated deduction program or constructed manually using a proof-checking system. This contradicts practice: even in mathematics most proofs are very far from being complete, and verification of programs usually checks only "principal" parts. Our goal here is to support this practice by some existing and new theory.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.