How to implement a fully declarative Horn logic?

Question

I would like to formalize some knowledge and fulfill requests in what can be called a fully declarative Horn logic (or a fully declarative Prolog). Can someone give some recommendations on how to implement it? I briefly listed the excellent description from the link above:

A formal language is Prolog (the main) language: a “program” is a set of rules and facts, as in Prolog (including functions and variables and basically containing only user-defined predicates).

Unlike Prolog, however, I am looking for a realistic and complete implementation related to the standard declarative semantics of logical programs --- the least Herbrand model (i.e., an inductively defined set of basic terms). In theoretical work on logical programming, this is usually the object of study, and it is well known that sound and a complete answer to queries can be achieved (in a "recursively enumerated" sense), for example, using SLD resolution provided the following conditions are met:

• fair search for matching rules (for example, depth search Prolog not );
• combining with occurs-checking "(checking that the variable does not occur in terms with which it is combined).

I am looking for a brief implementation that will build on existing capabilities, rather than reinvent the wheel. Two of the most promising areas that I see implement it as a Prolog meta-interpreter or as part of some theoretical evidence. Can someone with practical knowledge in these areas give some recommendations on how to implement it? Could this be easily implemented in miniKanren ?

---

My intentions are to formalize some knowledge in a completely declarative way. The most important characteristics of such a formalization are that it exactly corresponds to the mathematical concept of (monotonic) induction, so that knowledge and its properties are easily argued by inductive arguments.

Answer 1

This is a simple exercise to implement a Horn logic check in a few lines of the Prolog. Start with the Vanilla Meta Interpreter, then modify it to use the standard unify_with_occurs_check/2 predicate for all unifications and use the full search procedure. Iterative deepening of the depth of the first search is the easiest to implement.

Check out the @mat page for a couple of meta-interpreters in Prolog for inspiration.

Answer 2

Other pointers:

• Datalog has declarative semantics, but as a “Prolog without Functional Symbols” it is not a Prolog. See the excellent introduction, “What You Always Wanted to Know About Datalog (and Never Dared to Ask)” by Ceri, Gottlob, and Tanca, 1989. Available through CiteSeerX

• Prolog implementations that use tabling instead of searching by the depth of added declarativeity (plus other useful functions, as I understand it), for example XSB .