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