Guided Correctness Proofs of Logic Programs

E.I. Marakakis (Greece)


Correctness of logic programs, proof schemes, specifica tions, transformations, program schemata, verification.


This paper presents a correctness method of logic programs based on proof schemes. A proof scheme is a systematic plan of proof actions. A set of correctness proof schemes is presented. It is shown that the structure of a general logic program constructed by our schema-based method is re flected in the structure of its correctness proof. For each program schema of our method a proof scheme is proposed. The proof schemes corresponding to the design schemata are followed for the correctness of logic programs. Correct ness proofs in this approach are guided by the constructed logic programs.

Important Links:

Go Back