I was considering extending my Datalog work with customized evaluable predicates, but have decided against it. The safety guarantees of Datalog are just not worth giving up. To compensate, I have (very tentative) plans of building some sort of logic oriented bottom up computation engine -- think Cells without state. It would do fixed point work like Datalog, but with termination the programmer's problem. Like Datalog, it would still be recursive (using fixed point), but it would focus on *computation* not queries. I'll talk more about it when I get closer.
On Mon, Feb 9, 2009 at 2:58 PM, John Fries <john.a.fr...@gmail.com> wrote: > 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 -~----------~----~----~----~------~----~------~--~---
