Here's a Prolog implementation of a version of the language and I have been working on. I'm pretty sure that the algebraic setup is wrong (meaning that the calculus doesn't admit substitution), but the rest of the file is parametric in that. gist.github.com/laMudri/dd47ef
Conversation
Would be fun to try this in Makam! Been playing around with it recently and it's been a bunch of fun.
1
It's nice because you can actually do data types in it without needing to resort to comments (no mode checking though, sadly):
Quote Tweet
Replying to @brendanzab and @luctielen
This is what I have so far of my Makam work, if you're interested: gist.github.com/brendanzab/7a3
1
Yeah, I'm quite keen on trying this in another logic programming language. My wishlist is:
- Parametrised modules
- Static types, modes
- Functions/macros on terms
- Custom (infix) term notation
- Exhaustive testing of laws over finite domains
I guess Makam offers a few of these.
3
2
Yeah:
- modules are a bit lacking sadly
- static types but no mode checking
- there's staged metaprogramming, but no functions
- there's also an issue open discussing infix notation.
- not sure what you mean by "exhaustive testing" - kinda like model checking perhaps?
At any rate the author is pretty nice and responsive on the issue tracker and over email. Another thing to try might be abella-prover.org?
1
1
About exhaustive testing, I mean an implementation of the proof that every first order logic statement interpreted in a finite model is decidable. I suppose I might instead do this in some other tool, and copy the results back over to the logic program.