I looked at how to implement Prolog and was stumped until I found that SICP section.

So I ported it to JavaScript and gave it a Prolog-like syntax and made a web page where you could run the assignment but also exposed the inner workings, and it was one of the neatest things I've ever handed in as coursework.

(Thank you for reading the article, I also implemented microKanren before and it's insane how little code it takes to get full a logic programming engine going)

Same approach. I think an older version of the book it's freely available, or maybe the one on Scheme itself.

Scheme being homoiconic makes far easier to create quines.

I found it pretty interesting for that use case, although the learning curve isn't trivial for traditional devs.

https://www.openpolicyagent.org/

Note that I'm not an expert in any of this, I've just been reading about this kind of AI recently. I haven't actually done this myself.

Another example would be something like an Entity Component System. The moment it starts getting complex (i.e., you have fancy queries and joins), then you're actually implementing a really shitty relational programming engine, and you might as well just implement Datalog instead at that point and reap the benefits.

Other kinds of search problems are probably better tackled by constraint programming instead.

I am currently implementing a Datalog to PostgreSQL query engine at work as we want to experiment with modeling authorization rules in Datalog and then run authorization queries directly in the database. As I want to minimize the round trips to the database I use a different approach than yours and translate Datalog programs to recursive CTEs. These are a bit limited, so we have to restrict ourselves to linearly recursive Datalog programs, but for the purpose of modeling authorization rules that seems to be enough (e.g. you can still model things such as "permissions propagate from groups to group members").

(Also added a link to your article on what you can do with Datalog, excellent stuff, couldn't have written it better myself)

Twelf is quite elegant, although not as powerful as other proof assistants such as Coq. Proofs in Twelf are simply logic programs which have been checked to be total and terminating.

Edit: Here's a link to a short page in the manual which shows how termination checking works: https://twelf.org/wiki/percent-terminates/

The syntax of Twelf is a bit different from other logic languages, but just note that every rule must have a name and that instead of writing `head :- subgoal1, subgoal2, ..., subgoaln` you write `ruleName : head <- subgoal1 <- subgoal2 <- ... <- subgoaln`.

Also note that this approach only works for top-down evaluation because it still allows you to define infinite relations (e.g. the successor relation for natural numbers is infinite). Bottom-up evaluation will fail to terminate unless restricted to only derive facts that contribute to some ground query. I don't know if anyone have looked into that problem, but that seems interesting. It is probably related to the "magic sets" transformation for optimizing bottom-up queries, but as far as I understand that does not give any hard guarantees to performance, and I don't know how it would apply to this problem.

Look into Datafun: A total functional language that generalizes Datalog. Also be sure to watch Datafun author Michael Arntzenius's Strangeloop talk.

https://www.rntz.net/datafun/

https://www.youtube.com/watch?v=gC295d3V9gE

Yes you can add support for integers in various ways where termination is still guaranteed. The simplest trick is to distinguish predicates (like pred(X, 42)) from constraints (like X > 7). Predicates have facts, constraints do not. When checking that every variable in the head of a rule appears in the body, add the condition that it appears in a predicate in the body.

So if you have a predicate like age(X:symbol, Y:int), you can use its facts to limit the set of integers under consideration. Then, if you write:

age(X, A), A + 1 >= 18.

You'd get everyone that becomes an adult next year. Fancier solutions are also possible, for example by employing techniques from finite domain constraint solving.

> In this article, we study the convergence of datalog when it is interpreted over an arbitrary semiring. We consider an ordered semiring, define the semantics of a datalog program as a least fixpoint in this semiring, and study the number of steps required to reach that fixpoint, if ever. We identify algebraic properties of the semiring that correspond to certain convergence properties of datalog programs. Finally, we describe a class of ordered semirings on which one can use the semi-naïve evaluation algorithm on any datalog program.

It’s quite neat since this allows them to represent linear regression, gradient decent, shortest path (APSP) within a very similar framework as regular Datalog.

They have a whole section on the necessary condition for convergence (i.e. termination).

Funny enough, I made the same mistake you did back in the day. Used Prolog as the "boss" that just called back to Java as needed. My professor gave me a shitty grade because the idea was to make the opposite, a Java program that queries a Prolog database to make decisions, the Prolog part itself wasn't directly supposed to make any.

I was pissed at the time since I was showing off my Prolog skills which in a Logic Programming course I expected would give me a good grade, but that professor was 100% right. The power of logic programming is tainted when you mix it with IO and expect a specific ordering to the rule applications. Cuts are a sin.