## Expressing Natural Deduction in Logic Languages

I am looking at the order theoretic axioms for intuitionistic propositional logic, which form a Heyting algebra. I am thinking about the join rule:

C â‰¤ A     C â‰¤ B
---------------
C â‰¤ (A ^ B)


My understanding is the rule can be read both forwards and backwards. I initially encoded it like this:

rule(le(C, meet(A, B)), pair(le(C, A), le(C, B))).
rule(pair(le(C, A), le(C, B)), le(C, meet(A, B))).


But this needs the following additional rules to be defined:

rule(pair(A, B), pair(X, Y)) :- rule(A, X), rule(B, Y).
rule(pair(A, B), pair(Y, X)) :- rule(A, X), rule(B, Y).
rule(A, B) :- rule(A, C), rule(C,B).


The last of which is particularly problematic as it matches any 'A', and 'B' so results in dramatic increase in the search space, and results in a larger search depth to find the solution.

So as an alternative I want to encode the rules more natively, and I am thinking about extending the interpreter to allow conjunctions in the head, so the rules would be:

le(C, meet(A, B)) :- le(C, A), le(C, B).
le(C, A), le(C, B) :- le(C, meet(A, B)).


The implementation would match the first head struct as usual, and then would search the remaining goals for a match to the conjoined structs in the head (removing the matching goals).

Does this seem an efficient way to deal with this? Am I overlooking some way of rewriting the rules (although there is something to be said for keeping them close to the natural way of writing them)? Any suggestions for other ways to tackle this problem? I can't find any references to extending Prolog in this way, so I am concerned that this is problematic, or there is just a much simpler way to deal with it.

## Comment viewing options

### Implementations of Prolog

There's a 1984 collection of papers called Implementations of Prolog (TOC) edited by John A. Campbell. One of the papers in there is about logic programming with natural deduction rather than resolution. Unfortunately I can't remember which one it is.

This book also contains Nilsson's amazing paper "The World's Shortest Prolog Interpreter?" The interpreter in question is about half a page of Common-ish Lisp, and works on the principle of downward success continuations, recursing until it finds a solution. I had to fix a bunch of parenthesis typos, but it really does work.