Hello all :-) I've attached a fragment of my learning-some-miniKanren project, which is a theorem prover.
Running the file Chez Scheme, it spits out two proofs after about ~77 ms and ~34 ms, respectively. (It takes about ~10s in total using Chicken Scheme.) As far as I have been able to tell, if I re-order either the two calls from modus-ponens to proof-treeo or any of the calls from proof-treeo to axiomN, the program takes forever. My questions which I hope all of you lovely folks will help me answer: - Should "forever" be taken literally or figuratively? That is, do the reorderings cause divergence or merely a massive slow-down? - In either case, why? What are the steps performed by the miniKanren system, and why is that order-dependent? - How does one tell (at least some of the time) whether one's program is divergent? All of this order-dependence raises a scary question: are there some theorems which a prover like mine will find a proof of if the con- and disjuncts are ordered one way, but won't find a proof of if they're ordered some other way? How does one tell that a concrete proof search algorithm is complete (finds >=1 proof of all valid theorems)? (The axioms in my prover are Łukasiewicz's third systems, see https://en.wikipedia.org/wiki/List_of_logic_systems. IIRC my textbook listed that one as its single example of a complete and minimal system of axioms, FWIW.) -- 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.
theorem-prover.scm
Description: Binary data
