Sorry, I didn't mean to suggest that you held that opinion. In any case, I am still learning Clojure, so I think I should restrict myself to newbie questions until I am better at it. I hope I will have time to implement an open-world reasoner, which would help make the discussion concrete.
On Mon, Feb 9, 2009 at 4:34 AM, Rich Hickey <richhic...@gmail.com> wrote: > > > > On Feb 7, 2:25 pm, John Fries <john.a.fr...@gmail.com> wrote: > > I agree with Jeffrey that there is no reason to have just one option. > > I never suggested there ought to be only one option, nor am I trying > to argue against the utility of open-world reasoners. I merely asked, > given your assertion that open-world reasoners were more powerful than > Datalog, if they were therefor suitable for the tasks for which I > envisioned using Datalog, e.g. finding complete models, in a typical > data query manner. It seems from your description below that they > might not be, i.e. that it is supported but not efficient. > > Rich > > > Sometimes you want your reasoner to find a single model; sometimes you > want > > it to find all models (assuming you are reasoning over a finite set). > > > > I've appended a long rant about SAT-based reasoners and open-world > > semantics. I hope it is relevant, and apologize for the length. > > > > -John > > > > Initially, I had a lot of trouble understanding why the concept of > > satisfiability was relevant to reasoning. I just wanted to know whether > or > > not a sentence was true; whether or not it was satisfiable didn't seem > > relevant. Here's how you *could* use a SAT solver to answer a practical > > question (later I will explain why you would want to): > > > > Let's say you have a list of sentences A: > > A = ((man socrates) (for all X: man X -> mortal X)). > > A is your database of previous assertions. Now let's say that you want > to > > determine the truth state of a new sentence B: > > B = (mortal socrates) > > In other words, you want to know whether or not B is true, given all your > > previous assertions A. > > > > So you form two new sentences, Y & Z: > > X = (A and B) = ((man socrates) and (for all X: man X -> mortal X) and > > (mortal socrates)) > > Y = (A and (not B)) = ((man socrates) and (for all X: man X -> mortal X) > and > > (not (mortal socrates))) > > > > You then plug X into your SAT solver, and plug Y into your SAT solver. > > If X is satisfiable and Y is satisfiable, then we say that B's > truthstate, > > relative to A, is UNKNOWN. > > If X is satisfiable and Y is unsatisfiable, then we say that B's > truthstate, > > relative to A, is TRUE. > > If X is unsatisifiable and Y is satisfiable, then we say that B's > > truthstate, relative to A, is FALSE. > > If X is unsatisfiable and Y is unsatisfiable, then we say that B's > > truthstate, relative to A, is CONTRADICTION. > > > > In this example, I'm pretending we have a first-order logic SAT solver > (i.e. > > we can quantify, and our predicates take arguments), whereas usually we > only > > have a boolean logic SAT solver, but the former can be easily built upon > the > > latter (although it would be more efficient to build a first-order SAT > > solver). Also, the actual implementation can be much more optimized than > > this; there is usually overlapping work done during the evaluation of X > and > > Y. > > > > This example only shows you how to evaluate (truthstate A B). If you > wanted > > to find a *model* (i.e. a list of tuples of things that satisfy some > > sentence), then you would say something like "get X: red X" (i.e. get me > all > > X's that you can prove are red). In a system with finitely many things, > the > > vanilla unoptimized reasoner simply loops through each thing in the > system > > and asks for its truthstate: > > for each X: > > if (truthstate A (red X)) == TRUE: > > add X to output > > > > There can be situations where you would want, not just the things for > which > > the predicate is TRUE, but also the things for which the predicate is > > UNKNOWN. You can include that as a argument to your query. Also, there > is > > a separate mechanism for performing default reasoning (which I am eliding > > here because this is already a pretty long rant). > > > > Why go through all this trouble to get open-world semantics? Why not > just > > use a close-world reasoner? First, I think open-world semantics does a > > better job of mimicing human reasoning. If humans don't know that a > > sentence is true, they don't generally conclude that it's false. Second, > > basing your reasoner on a SAT solver makes a lot of sense > computationally. > > SAT is a hard problem (NP-complete), but so much work has been done on it > > that in practice we can solve very large instances efficiently (and any > SAT > > problem is solvable given enough time and memory). The underlying SAT > > solvers seem to be improving at a tremendous rate, so a system that > > interfaces to them benefits from all that work. > > > > -John > > > > On Thu, Feb 5, 2009 at 2:04 PM, Jeffrey Straszheim < > > > > straszheimjeff...@gmail.com> wrote: > > > 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 -~----------~----~----~----~------~----~------~--~---
