E. Marakakis and N. Papadakis (Greece)
Interactive verifier, logic programs correctness, proofchecker.
This paper presents the design of an interactive verifier or proof checker for logic programs. These logic programs are constructed by a schema-based method. This design is divided in the design of the proof checker, the design of the interface and the representation of the knowledge base. The emphasis in the design of the interface is on the provision of the required assistance to the user for the proof of a theorem. In addition, it provides support for the update of the knowledge base. Special importance in the design is on the performance by the verifier of tedious, trivial and time consuming tasks. The difficult proof decisions are taken by the user, then, our proof checker applies these proof decisions. The main design criterion for the knowledge representation is the support for an efficient and modular implementation of the verifier.
Important Links:
Go Back
