reposted to correct a mistake in my use of X, Y and Z:
---------------
I agree with Jeffrey that there is no reason to have just one option.
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:
Y = (A and B) = ((man socrates) and (for all X: man X -> mortal X) and
(mortal socrates))
Z = (A and (not B)) = ((man socrates) and (for all X: man X -> mortal X) and
(not (mortal socrates)))
You then plug Y into your SAT solver, and also plug Z into your SAT solver.
If Y is satisfiable and Z is satisfiable, then we say that B's truthstate,
relative to A, is UNKNOWN.
If Y is satisfiable and Z is unsatisfiable, then we say that B's truthstate,
relative to A, is TRUE.
If Y is unsatisifiable and Z is satisfiable, then we say that B's
truthstate, relative to A, is FALSE.
If Y is unsatisfiable and Z 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 Sat, Feb 7, 2009 at 11:25 AM, John Fries <john.a.fr...@gmail.com> wrote:
> I agree with Jeffrey that there is no reason to have just one option.
> 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
-~----------~----~----~----~------~----~------~--~---
