Completeness of category-based equational deduction (abstract)

Equational deduction is generalised within a category-based abstract model theory framework, and proved complete 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. Applications include many and order sorted [conditional] equational logics, Horn clause logic, equational deduction modulo a theory, constraint logics, and more, as well as any possible combination among them. In the cases of equational deduction modulo a theory and of constraint logic the completeness result is new.

One important consequence is an abstract version of Herbrand's Theorem, which provides an abstract model theoretic foundations for equational and constraint logic programming.

back to Selected Publications