Herbrand Theorems in arbitrary institutions

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 developed in Institution-independent Ultraproducts. The institution-independent concept of substitution is developed for the first time here, being one of the main contributions of this paper.

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.

---