Herbrand Theorems in arbitrary institutions
back to Selected Publications
The logic programming paradigm in its purely logical
form can be described as follows: ``Given a universal Horn (finite)
presentation $(\Sigma,E)$ (called `program', with $\Sigma$ the
`signature' of the program, i.e., the set of its symbols, and $E$ the
set of $\Sigma$-sentences) and an existentially quantified conjunction
of atoms $\rho$ (called `query') in $\Sigma \cup Y$ (for $Y$ a new set
of `logical variables'), find a `solution' $\psi$ for $\rho$,
i.e., values for the variables $Y$, such that the corresponding
instance $\psi[\rho]$ of $\rho$ is satisfied by $(\Sigma,E)$.''
In other words, we need that $(\Sigma,E) \models (\exists Y)\rho$.
In the most conventional form, logic programming is considered over
unsorted first order logic without equality, less conventional forms
of logic programming extends this to multiple
sorts, or even considers first order logic with equality as underlying
logic, this being considered as a new related paradigm, and known
under the name of `equational logic programming'.
However, a careful look at the logic programming paradigm shows its
semantical folundations are essentially institution-independent.
The basic logic programming concepts, query, solutions, solution
forms, and the fundamental results, such as Herbrand theorems, can be
developed over any institution by employing institution-independent
concepts of variable, substitution, quantifiers, atomic formula\ae,
most of them being part of the `internal logic' of institutions
The institution-independent concept of substitution is developed for
the first time here, being one of the main contributions of this
Our work sets foundations for an uniform development of logic
programming over a large variety of computing science logics, which
opens the door for a clean combination between logic programming and
various other computing paradigms.
In this `institution-independent' framework we also discuss some basic
modularisation issues for logic programming.