The basic principle is that miniKanren uses a complete, interleaving search that is capable of enumerating all answers. If, however, an answer does *not* exist, miniKanren *may* diverge.
This paper gives a detailed explanation of how individual arithmetic relations may be written to avoid divergence, by incorporating constraints on the term sizes into the arithmetic relations: http://webyrd.net/arithm/arithm.pdf The paper gives code in Prolog--you can find the equivalent code in miniKanren in my dissertation: https://github.com/webyrd/dissertation-single-spaced/raw/master/thesis.pdf We can also perform arithmetic using finite domain constraints, using a specialized constraint solver. For details on miniKanren's search, you might look at: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf or http://okmij.org/ftp/papers/LogicT.pdf Cheers, --Will On Wednesday, September 7, 2016 at 1:31:14 PM UTC-6, Mr. Gogo wrote: > > I'm coming from a background of satisfiability (i use model checkers). > When the negation of claim is satisfiable model checkers gives a > counterexample. I know one trivial way, block a counterexample(add negation > to the conjunction with the query) and get as many as u like but its a > laborious task. > > > How run * in minikanren works that gives all the possible models ? For > example how you can you get for all possible proofs of 2 + 3 = 5 ?? What's > happening under the hood? What is the basic principle ? > > This Looks damn :) > -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
