On definite program answers and least Herbrand models

A sufficient and necessary condition is given under which least Herbrand models exactly characterize the answers of definite clause programs.

Completeness and Herbrand theorems for nominal logic

Nominal logic is a variant of first-order logic in which abstract syntax with names and binding is formalized in terms of two basic operations: name-swapping andfreshness. It relies on two important principles: equivariance (validity is preserved by name-swapping), and fresh name generation (“new” or fresh names can always be chosen). It is inspired by a particular class of models for abstract syntax trees involving names and binding, drawing on ideas from Fraenkel-Mostowski set theory: finite-support models in which each value can depend on only finitely many names.Although nominal logic is sound with respect to such models, it is not complete. In this paper we review nominal logic and show why finite-support models are insufficient both in theory and practice. We then identify (up to isomorphism) the class of models with respect to which nominal logic is complete: ideal-supported models in which the supports of values are elements of a proper ideal on the set of names.We also investigate an appropriate generalization of Herbrand models to nominal logic. After adjusting the syntax of nominal logic to include constants denoting names, we generalize universal theories to nominal-universal theories and prove that each such theory has an Herbrand model.

Category-based constraint logic

The research reported in this paper exploits the view of constraint programming as computation in a logical system, namely constraint logic. The basic ingredients of constraint logic are: constraint models for the semantics (they form a comma-category over a fixed model of ‘built-ins’); generalized polynomials in the role of basic syntactic ingredient; and a constraint satisfaction relation between semantics and syntax. Category-based constraint logic means the development of the logic is abstract categorical rather than concrete set theoretical.We show that (category-based) constraint logic is an institution, and we internalize the study of constraint logic to the abstract framework of category-based equational logic, thus opening the door for considering constraint logic programming over non-standard structures (such as CPO's, topologies, graphs, categories, etc.). By embedding category-based constraint logic into category-based equational logic, we integrate the constraint logic programming paradigm into (category-based) equational logic programming. Results include completeness of constraint logic deduction, a novel Herbrand theorem for constraint logic programming characterizing Herbrand models as initial models in constraint logic, and logical foundations for the modular combination of constraint solvers based on amalgamated sums of Herbrand models in the constraint logic institution.