Correctness of logic programs using proof schemes

Article type: Research Article

Authors: Marakakis, Emmanouil^{; *} | Papadakis, Nikos

Affiliations: Sciences Department, Technological Educational Institute of Crete, Heraklion, Greece

Correspondence: [*] Corresponding author. E-mail: mmarak@cs.teicrete.gr

Abstract: The correctness of logic programs which are constructed by a schema-based method is presented in this paper. This schema-based method constructs typed, moded logic programs by stepwise top-down design using five program schemata, data types and modes. Correctness proofs in this approach are guided by the constructed logic programs. A proof scheme is proposed for each program schema. It is claimed that the structure of a logic program constructed by this schema-based method is reflected in the structure of its correctness proof. The proof schemes which correspond to design schemata are followed in the correctness proofs of logic programs.

Keywords: Correctness of logic programs, specifications, transformations, proof schemes, program schemata

DOI: 10.3233/KES-2012-0242

Journal: International Journal of Knowledge-based and Intelligent Engineering Systems, vol. 16, no. 3, pp. 185-198, 2012