A question on transforming (some) logical program as a linear system of equalities/inequalities:
Say proposition X=0 for false, X=1 for true, and likewise for all propositions, then X → Y (X leads to Y) can be written as
- X + Y >= 0
As above, one may transform (some) logical program into a linear system of equalities/inequalities. Has it been applied to logical program solution/deduction/abduction? Any good, basic, definitive reference paper(s) on the approach?
I am not sure that I understand exactly what you mean. That notation usually means “X can be rewritten as Y”. It’s a rewrite rule. It seems like you use it in a different way
No - X implies Y says nothing about Y, if X is false.
X and Y can be completely different expressions.
Ah ok. So it’s a different thing. I thought it was a rewrite rule. But it’s logical implication
Still this notation remains obscure to me, but it’s not a big issue. Just for the sake of discussion
PS: the formatting didn’t work right…i don’t know why the minus sign was replaced by a dot 
Hey I had edited the post — I had had to prepend the minus sign with a backslash, otherwise it will be displayed as a black dot for bullet point. Not sure why you still see the black dot though.
Thanks very much. clpBNR does seem to help.
A question for now. On https://github.com/ridgeworks/clpBNR it is stated its advantage consists in
?- 1.21 =:= 1.1*1.1.) In particular the add and multiply operations are non-associative and non-distributive. Relational interval arithmetic in CLP(BNR) (and some others) ensures that computed intervals contain the mathematically correct real value.How crucial are the above points, if for a logical program, most real values are bounded, but can take value NaN (not-a-value), or infinity?
The above two advantage come at cost of how much additional compute, generally speaking?
First point is not to conflate reals and floating point values; the latter is an imperfect approximation of reals.
NaN’s are not real numbers, as the name would imply, so they’re not legal in the “real” domain of clpBNR. However infinities are included in the real domain so a real interval can be bounded by an infinity, but it’s just a bound. When applied, constraints cause the domain of a “real” to narrow (a domain never gets wider), so infinite bounds generally disappear in the course of a computation.
New bounds are the intersection of the current bounds and the computed bounds as defined by constraints. Now the computed bounds may produce NaN’s or infinities, but that just generally means the interval doesn’t narrow as a result of the computation.
I think the above points are fairly crucial for logical correctness which, to me at least, implies mathematical correctness (and completeness) over the domain of real numbers.
Off the top of my head a fair amount, all things considered. A primitive interval relation like {Z == X+Y} requires 6 arithmetic ops (including rounding control if bounds are floating point) plus domain intersection for a total of 9. Plus the additional overhead of running an IA virtual machine implemented in Prolog. (In general the clpBNR VM is responsible for propagating changes in one real value to co-constrained values and checking for consistency.) I typically observe 100,000-200,000 narrowing ops per second, so I’d guess 1-2 orders of magnitude over functional Prolog arithmetic.
A simple interval arithmetic library which just preserves correctness without all the constraint stuff would obviously do better. And there are a number of IA libraries available which should provide background information to help answer your question.
Not a big issue. It’s a good thing that you (being a young student, I assume) have this kind of intellectual ambitions. Last thing I did in “programming” was creating a Snake game in Python (following a tutorial on Youtube) and I have to say that I’m quite happy with the result…Tic-Tac-Toe should come next 
maybe a ralated paper: Taisuke Sato. A linear algebraic approach to datalog evaluation, TPLP 2017, doi:10.1017/S1471068417000023
Matrix operations over reals are employed there.