There is no reason to have just one option. On Thu, Feb 5, 2009 at 3:59 PM, Rich Hickey <richhic...@gmail.com> wrote:
> > Thanks for the pointer to Kodkod - it looks very interesting. > > I wonder if we aren't talking apples and oranges though. Datalog may > be a basic reasoner, but it's a simple recursive query language for > data. Can you even get all results out of a SAT solver or do they stop > when satisfiable? > > It's for this query purpose that I envisioned primary use of Datalog, > although I can certainly see the utility of more powerful reasoners > too. > > Rich > > On Feb 5, 12:22 pm, John Fries <john.a.fr...@gmail.com> wrote: > > Yes. I can make a strong endorsement for Kodkod, a Java-based relational > > model finder.http://alloy.mit.edu/kodkod/ > > I used it fairly extensively last year to solve scheduling problems, and > > I've corresponded with its creator. > > > > One problem with Datalog-style reasoners is that, because they want to > > guarantee a certain execution time, they give up much of the > expressiveness > > of relational logic. Instead, Kodkod provides the correct interface to > > relational logic, and relies on an underlying SAT solver (such as > MiniSat) > > to solve the problems in a reasonable amount of time. This has proven to > be > > a good approach, because SAT solvers have been improving at a tremendous > > rate over the last 10 years, and are now blazingly fast. > > > > Another advantage of Kodkod over, say, FaCT++ or Pellet (which also > provide > > open-world semantics) is that you are not tied into all the assumptions > of > > the semantic web (OWL, RDF, XML, etc), which can get pretty clunky when > all > > you want is an in-memory reasoner. You only have to be reasonably > > comfortable with relational logic (e.g. "for all x: Red x") to be able to > > use Kodkod. > > > > The only deficiency I found in Kodkod was that, because the author wanted > to > > support an audience whose primary language was Java, the user must > express > > their queries using a Java class-based syntax. But this seems like a > > perfect use of Clojure, which could provide a much more natural query > > syntax. > > > > On Thu, Feb 5, 2009 at 4:29 AM, Rich Hickey <richhic...@gmail.com> > wrote: > > > > > On Feb 4, 5:22 pm, John Fries <john.a.fr...@gmail.com> wrote: > > > > Guaranteed-termination is very desirable. However, you can have > > > guaranteed > > > > termination with an open-world assumption just as well. And I think > an > > > > open-world assumption does a better job of mimicking human reasoning. > > > > > Do you have a specific reasoner/algorithm in mind? > > > > > Rich > > > --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en -~----------~----~----~----~------~----~------~--~---
