John,
Thanks for forwarding the paper. This is the
first I've seen of it. Unfortunately, for
reasons I don't understand, they used old
versions of the ontologies from
Teknowledge. Those haven't been the newest
versions for several years now. In particular,
several axioms about ListFn were fixed years
ago. They say there are "numerous
inconsistencies", but don't say what they are. I
also don't know why they didn't let me know what
they were so they could be fixed. I'll try to find out. (01)
Adam (02)
At 08:16 AM 3/9/2006, John A. Bateman wrote:
>Forwarded comments/info/papers.
>
>-------- 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>
>
>
>--
>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
>
>
>
>Message-ID: <44086671.6040603@xxxxxxxxxxxxxxxxxxxxxxxx>
>Date: Fri, 03 Mar 2006 16:53:21 +0100
>From: Till Mossakowski <till@xxxxxxxxxxxxxxxxxxxxxxxx>
>User-Agent: Mozilla Thunderbird 1.0.2 (X11/20050322)
>X-Accept-Language: en-us, en
>MIME-Version: 1.0
>To: andersen@xxxxxxxxxxxxxxxxx
>CC: "John A. Bateman" <bateman@xxxxxxxxxxxxx>,
> Klaus Luettich <luettich@xxxxxxxxxxxxxxxxxxxxxxxx>
>Subject: Re: [Fwd: Question]
>References: <44046FFB.3090601@xxxxxxxxxxxxx>
>In-Reply-To: <44046FFB.3090601@xxxxxxxxxxxxx>
>Content-Type: multipart/mixed;
> boundary="------------080803010204090906080501"
>
>Hi Bill,
>
>John has forwarded the mail below to me.
>
>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).
>
>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.
>
>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.
>
>Greetings,
>Till
>
>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.
>
>>-------- 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
>>
>
>
>--
>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
>
>
>
>
> _________________________________________________________________
>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 (03)
----------------------------
Adam Pease
http://www.ontologyportal.org - Free ontologies and tools (04)
_________________________________________________________________
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 (05)
|