zbMATH — the first resource for mathematics

A logical analysis of modules in logic programming. (English) Zbl 0681.68022
This paper is concerned with an extension of positive Horn clause logic by allowing implications in goals and in bodies of clauses. It shows the use of this extension in storing successful goals and in implementing (parametric) modules in a purely logical fashion. Also both model theory and proof theory are provided, and in particular the relation of the logic with intuitionistic and minimal logic is established. Finally a weak notion of negation is examined that is easily implemented in the logic, and it is showed how disjunctions can be eliminated from programs in the language concerned.
Reviewer: J.-J.Ch.Meyer

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N01 General topics in the theory of software
68N25 Theory of operating systems
68Q55 Semantics in the theory of computing
Full Text: DOI