Forwarded comments/info/papers. (01)
-------- Original Message --------
Subject: [Fwd: Re: [Fwd: Question]]
Date: Mon, 06 Mar 2006 17:32:17 +0100
From: Till Mossakowski <till@xxxxxxxxxxxxxxxxxxxxxxxx>
To: John Bateman <bateman@xxxxxxxxxxxxx> (02)
--
Till Mossakowski Phone +49-421-218-4683
Dept. of Computer Science Fax +49-421-218-3054
University of Bremen till@xxxxxx
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till (03)
--- Begin Message ---
Hi Bill, (01)
John has forwarded the mail below to me. (02)
Let me first note that it is even possible to deal with large
unstructured masses of FOL, as the attached paper shows (they
have used Vapmire to find numerous inconsistencies in SUMO). (03)
But then let me point out the usefulness of structuring, like
it is present in the CASL languague (www.cofi.info), but also
in many theorem provers, e.g. Isabelle and KIV (the latter not
to be confused with KIF :-). Hierarchical structuring of theories
may help in structuring the proof search space. Some initial
thoughts in this direction are made in section 9.3 of the
second attached paper (about a combination of the provers Isabelle
and SPASS), although the application of this to automated FOL provers
like SPASS seems to be an open research problem, and one probably
does not want to use an interactive prover (like Isabelle) alone .
for proving theorems about large ontologies. (04)
Structuring is even more crucial for proving consistency of
ontologies. It is much easier to prove inconsistency (i.e.
derive false using a theorem prover) than prove consistency
(e.g. by constructing a finite model using a SAT solver, or
by using a resolution prover for finding a saturated set of
clauses not containing the empty clause). We did not manage to
prove consistency of DOLCE with such techniques, and have
just prepared a grant proposal that proposes to use structuring
techniques (e.g. the Robinson joint consistency theorem).
The crucial problem here is to develop techniques for establishing
conservativity of theory extensions. (05)
Greetings,
Till (06)
P.S.
Can you tell me how to subscribe to uos-convene@xxxxxxxxxxxxxxxx?
I have some comments to some mails there, but have not found
a possibility to subscribe. (07)
> -------- Original Message --------
> Subject: Question
> Date: Tue, 28 Feb 2006 09:48:14 -0500
> From: Bill Andersen <andersen@xxxxxxxxxxxxxxxxx>
> To: John A.Bateman <bateman@xxxxxxxxxxxxx>
>
> John,
>
> Your description of your work on the UOS list was very interesting.
> That's a big mass of FOL and maybe even modal FOL (I forget whether
> DOLCE has it or not). For my own edification, does any of this
> actually work? How do you overcome the problems of doing theorem
> proving over such a large mass of axioms with anything but a trivial
> amount of "data" and get results in anything close to the time
> required to support "communication" that wouldn't drive users to
> suicide? Cycorp has also a similar problem.
>
> .bill
>
> PS - If this all sounded impertinent, don't worry. It's just my
> style – you can ask Barry for confirmation.
>
>
> Bill Andersen (andersen@xxxxxxxxxxxxxxxxx)
> Chief Scientist
> Ontology Works, Inc. (www.ontologyworks.com)
> 3600 O'Donnell Street, Suite 600
> Baltimore, MD 21224
> Office: 410-675-1201
> Cell: 443-858-6444
>
>
>
> (08)
--
Till Mossakowski Phone +49-421-218-4683
Dept. of Computer Science Fax +49-421-218-3054
University of Bremen till@xxxxxx
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till (09)
I_Horrocks-A_Voronkov-FOIKS06.pdf
Description: Adobe PDF document
Isabelle-SPASS.pdf
Description: Adobe PDF document
--- End Message ---
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/uos-convene/
To Post: mailto:uos-convene@xxxxxxxxxxxxxxxx
Community Portal: http://ontolog.cim3.net/
Shared Files: http://ontolog.cim3.net/file/work/UpperOntologySummit/uos-convene/
Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?UpperOntologySummit (01)
|