<p>More pointers:</p>

<ul>
<li><p><a href="https://en.wikipedia.org/wiki/Datalog" rel="nofollow">Datalog</a> has declarative semantics, but as a "Prolog without function symbols" it is not Prolog. See the excellent intro <em>"What You Always Wanted to Know About Datalog (And Never Dared to Ask)"</em> by Ceri, Gottlob and Tanca, 1989. Available via <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.210.1118&amp;rank=1" rel="nofollow">CiteSeerX</a></p></li>
<li><p>Implementations of Prolog that use <a href="https://www.google.com/search?q=tabled+logic+programming&amp;ie=utf-8&amp;oe=utf-8" rel="nofollow">tabling</a> instead of depth-first search for added declarativeness (plus other nice features as I understand), like <a href="http://arxiv.org/abs/1012.5123" rel="nofollow">XSB</a>.</p></li>
</ul>
How to implement fully-declarative Horn logic?
<p>I would like to formalize some knowledge and execute queries in what may referred to as fully-declarative <a href="http://www.w3.org/2005/rules/wg/wiki/Horn_Logic" rel="nofollow">Horn logic</a> (or, fully-declarative Prolog). Could anyone provide some guidelines on how to implement it? I briefly recap the fine description from the link above:</p>

<p>The formal language is that of (the core of) Prolog: a "program" is a set of rules and facts as in Prolog (including functions and variables and basically, containing only user defined predicates).</p>

<p>In contrast to Prolog, however, I am looking for an implementation that is sound and complete with respect to the standard declarative semantics of logic programs --- the least Herbrand model (i.e., the inductively defined set of ground terms). In theoretical work on logic programming this is usually the object of study, and it is well known that a sound and complete answer to queries can be attained (in the "recursively-enumerable" sense), for example, using SLD-resolution subject to the following conditions:</p>

<ul>
<li><strong>fair</strong> search for matching rules (e.g., Prolog's depth-first search is <strong>not</strong> fair);</li>
<li>unification with "<strong>occurs-check</strong>" (checking that a variable doesn't occur in a term with which it is unified).</li>
</ul>

<p>I am looking for a concise implementation that would build on existing capabilities, rather than inventing the wheel. Two of the more promising directions that I see are implementing it as a meta-interpreter of Prolog, or as part of some theorem prover. Could anyone with practical knowledge in these domains provide some guideline on how to implement it? Can it be easily implemented in <a href="http://minikanren.org/" rel="nofollow">miniKanren</a>?</p>

<hr>

<p><em>My intentions are to formalize some knowledge in a fully-declarative manner. The crucial characteristics of such a formalization is that it precisely corresponds to the mathematical notion of (monotone) induction, so that the knowledge and it's properties can be easily reasoned about with inductive arguments.</em></p>