Incomplete Proofs and Program Synthesis

Logic-Based Program Synthesis: State of the Art and Future Trends

Volume

Papers from the 2002 AAAI Spring Symposium

Contents

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.