CATEGORY−BASED SEMANTICS FOR EQUATIONAL AND CONSTRAINT LOGIC PROGRAMMING

Abstract

This thesis proposes a general framework for educational logic programming, called category-based educational logic by placing the general principles underlying the design of the programming language Eqlog and formulated by Goguen and Meseguer into an abstract form. This framework generalises equational deduction to an arbitrary category satisfying certain natural conditions; completeness is proved under a hypothesis of quantifier projectivity, using a semantic treatment that regards quantifiers as models rather than variables, and regards valuations as model morphisms rather than functions. This is used as a basis for a model theoretic category-based approach to a paramodulation-based operational semantics for equational logic programming languages.