Search code examples
encodingprologlogicdataloglogicblox

How could I encode "implies" logic in LogicBlox?


I would like to encode "implies" logic in LogicBlox. I have a predicate:

Number(n),hasNumberName(n:i)->int(i).
isTrue[n] = i -> Number(n), boolean(i).

And I add some data in that predicate:

+Number(1).

Now, I want to create number 2 and number 3, and the truth value for these two number following this logic rule:

If isTrue[1] is true, then isTrue[2] is true or isTrue[3] is true. (isTrue[1] implies (isTrue[2] or isTrue[3]))

So I create a predicate:

 implies[n1,n2,n3] = e -> Number(n1), Number(n2), Number(n3),boolean(e).

Then I try to create a rule like that:

isTrue[n2] = true;isTrue[n3] = true <- isTrue[n1] = true,implies[n1,n2,n3] = true.

But LogicBlox reports:"error: disjunction is not supported in the head of a rule "

So how can I encoding this implies logic in LogicBlox?


Solution

  • From your question it looks like you're asking this question with a Prolog background. If so, then it might be helpful to read a Datalog introduction, for example "What you always wanted to know about Datalog (and never dared to ask)".

    The logic you want to express is on purpose not allowed in Datalog, because it requires a solving or search strategy. As opposed to Prolog, Datalog is on purpose restricted in the computational complexity of the programs you can express. As a result of these restrictions it meets important requirement for use in a database management system, most importantly supporting very large data sets. The computational complexity restrictions will be more clear after reading a good introduction to Datalog.

    People have studied extensions of Datalog to allow more programs to be expressed (without going to full Prolog, which would result in a more procedural semantics). This particular example is called "Disjunctive Datalog". The hits on Google look good for this if you want to read more. LogicBlox does (at least currently) not implement Disjunctive Datalog because our primary objective is to be a scalable database management system.

    LogicBlox does support using a solver for specific programs. A typical example is the knapsack problem. If your problem is expressible as an optimization problem (it almost certainly is, but the formulation usually requires some creativity for things that are not conventional optimization problems), then you could use this feature. The solver functionality is not very well documented in publicly available material yet. Please reach out to us directly if you would like to give this a try.