6:49:42merskiasaAnyone here able to write an IRC bot like this: http://www.omnimaga.org/computer-projects-and-ideas/haroldbot-%28theorem-prover-solver%29
6:55:47merskiasaThe thing has four modes: 1) solve, 2) quantified solve, 3) calculation and 4) prove.
6:56:10merskiasa1) solve and 4) prove are basically identical, because they differ only in predicate to prove (equality for solve and arbitrary comparison for prove). Prove needs a way to interpret results
6:56:35merskiasaI know how to formulate problem in CNF/BDD form. I also know how to use SAT solver. I haven't implemented interpretation of unsatisfability results.
6:56:53merskiasabeach, you interested in the project?
9:14:40merskiasa<merskiasa> Anyone here able to write an IRC bot like this: http://www.omnimaga.org/computer-projects-and-ideas/haroldbot-%28theorem-prover-solver%29
9:14:48merskiasa<merskiasa> The thing has four modes: 1) solve, 2) quantified solve, 3) calculation and 4) prove.
9:14:49merskiasa<merskiasa> 1) solve and 4) prove are basically identical, because they differ only in predicate to prove (equality for solve and arbitrary comparison for prove). Prove needs a way to interpret results
9:14:49merskiasa<merskiasa> I know how to formulate problem in CNF/BDD form. I also know how to use SAT solver. I haven't implemented interpretation of unsatisfability results.
9:42:05shka_it is rather messy and if i would have more time i would write my own (with thread safety and perhaps even parallel unification built in) but it should be enough for you
14:14:16BepBepAnyone have an opinion on using TXR or Guile for scripting?
14:23:59edgar-rftBepBep, we of course suggest using Common Lisp instead :-)
14:24:19dloweThe "any lisp goes" channel is ##lisp
14:29:21beachBepBep: In other words, this channel is dedicated to Common Lisp.
14:30:34beachBepBep: Choice 1: Write your entire application in Common Lisp. Choice 2 (if you already have an application written in some static language): Use ECL.
14:32:20XachI have a long-running interest in exposing cl-js as a scripting system for a Common Lisp application
14:33:05beachXach: What makes you need anything other than Common Lisp itself?