Logic variables support for .NET

Question

I am looking for a library/assembly that allows me to work with logical variables in F#. I want to avoid reinventing the wheel in implementing the required union-find datastructure, unification code and so on.

I have found Prolog.NET, but the manual is a bit sparse. I do not want a full-fledged Prolog implementation, but only its treatment of logical variables and the manual is kind of lacking in that respect.

Here's what I want to be able to do:

• declare new logical variables
• bind a log.var. to a term (perferably the library allows complete Herbrand terms for that)
• equalize log.vars. (i.e. unification)
• meta-treatment of log.vars. (is it ground? to which other log.vars. has it been equalized?...)
• eventually, the library even supports matching, i.e. one-sided unification.

Does anyone know any library that does all this, or libraries that might at least be used as a starting point?

Answer 1

I don't know a library offhand that does what you want. However, I do have an implementation of "union-find in F#" in this blog entry. And from my college days, I seem to recall some popular book on Scheme had a basic unification algorithm in it which I used to code up a 'mini-prolog' implementation back in the day. So I feel like this is something that someone with the right experience could put together in a weekend, in case someone out there is looking for a project. (Perhaps I'll add it to my own weekend TODO list.)

Answer 2

Mini-Kanren has been implemented for Scala. I'm not a .NET programmer, and can't say how useful this is to you, but Mini-Kanren fits your requirements in terms of a programmatic logic-variable language: if the Scala embedding in .NET has properties compatible with what you are after, then you should be there.

Answer 3

I have a basic embedding of logic programming in F#. I developed it for the course I teach on "Programing Paradigms", which uses F# throughout and includes a couple of lectures on logic programming.

The code uses imperative updates to reflect substitutions due to unification, and it uses success continuations. So it is relatively different from, e.g., Kanren.

I'm not sure how much sense the notes will make by themselves, but you can find this embedding at the end of: http://undergraduate.csse.uwa.edu.au/units/CITS3242/16-logic-prog.pdf

I can provide a refined version of this embedding on request.