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
-~----------~----~----~----~------~----~------~--~---
