Extending Horn clause theories by reflection principles

2005 ◽  
pp. 400-413 ◽  
Author(s):  
Stefania Costantini ◽  
Pierangelo Dell'Acqua ◽  
Gaetano A. Lanzarone
Keyword(s):  
Horn Clause ◽  
Reflection Principles

HoIce: An ICE-Based Non-linear Horn Clause Solver

2018 ◽  
pp. 146-156 ◽  
Author(s):  
Adrien Champion ◽  
Naoki Kobayashi ◽  
Ryosuke Sato
Keyword(s):  
Horn Clause ◽  
Non Linear

Completeness of category-based equational deduction

1995 ◽  
Vol 5 (1) ◽  
pp. 9-40 ◽  
Author(s):  
Răzvan Diaconescu
Keyword(s):  
Logic Programming ◽  
Model Theory ◽  
Constraint Logic Programming ◽  
Horn Clause ◽  
Abstract Model ◽  
Abstract Model Theory ◽  
Completeness Result ◽  
Semantic Treatment ◽  
Theory Framework ◽  
Deduction Modulo

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 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 foundation for equational and constraint logic programming.

Sign in / Sign up

Export Citation Format

Share Document