Ask HN: How to test or proove logic programming?

3 points by piotr-yuxuan ↗ HN
I've been writing some logic code in core.logic, a clojure port of Will Byrd's miniKanren. To make sure my program is correct for any suitable input (not merely for the example I provided during development), I feel I should write some proof.

Do you know any tool / any manual method to proove a programm written with logic programming? I'm reading the Reasoned Schemer to get further acquainted with logic programming, I could translate my logic Clojure code into logic Scheme if necessary.

In case you'd ask for any code example, you can have a loook here: https://github.com/piotr-yuxuan/polygam However, just keep in mind it's a big mess currently under heavy development.

I already know a (very tiny) bit about formal proof of a program and I love to learn. Thanks in advance for your kind replies.

2 comments

[ 3.0 ms ] story [ 17.6 ms ] thread
I'm sorry I know nothing about core.logic. However, if you are familiar with Prolog, and sufficiently motivated to work through cited references, this paper is a good place to start. [1]

[1] https://arxiv.org/abs/1412.8739

Great, thank you very much for your help :-)