Correctness of logic programs using proof schemes

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.