Re: "explanations" in cwm, vocabulary for proof exchange

On Fri, 2003-04-25 at 09:24, Drew McDermott wrote:
[...]
> Of course, neither observation applies to a machine checking a
> machine-produced proof, which should be quite easy.

I'm much more interested in machine checking of machine-produced
proofs.

[[
The Semantic Web has a different set of goals from most systems of
logic. As Crawford and Kuipers put it in [Crawf90],

        [...]a knowledge representation system must have the following
        properties: 
             1. It must have a reasonably compact syntax.
             2. It must have a well defined semantics so that one can
                say precisely what is being represented.
             3. It must have sufficient expressive power to represent
                human knowledge.
             4. It must have an efficient, powerful, and understandable
                reasoning mechanism
             5. It must be usable to build large knowledge bases.
        
        
        It has proved difficult, however, to achieve the third and
        fourth properties simultaneously.
        
The semantic web goal is to be a unifying system which will (like the
web for human communication) be as un-restraining as possible so that
the complexity of reality can be described. Therefore item 3 becomes
essential. This can be achieved by dropping 4 - or the parts of item 4
which conflict with 3, notably a single, efficient reasoning system. The
idea is that, within the global semantic web, there will be a subset of
the system which will be constrained in specific ways so as to achieve
the tractability and efficiency which is no necessary in real
applications. However, the semantic web itself will not define a
reasoning engine. It will define valid operations, and will require
consistency for them. On the semantic web in general, a party must be
able to follow a proof of a theorem but is not expected to generate one.

(This fundamental change goals from KR systems to the semantic web is
loosely analogous with the goal change from conventional hypertext
systems to the original Web design dropping link consistency in favor of
expressive flexibility and scalability.The latter did not prevent
individual web sites from having a strict hierarchical order or matrix
structure, but it did not require it of the web as a whole.)

If there is a semantic web machine, then it is a proof validator, not a
theorem prover. It can't find answers, it can't even check that an
answer is right, but it can follow a simple explanation that an answer
is right. The Semantic Web as a source of data should be fodder for
automated reasoning systems of many kinds, but it as such not a
reasoning system.
]]
 -- The Semantic Web as a language of logic
 Tim Berners-Lee Date: 1998
 http://www.w3.org/DesignIssues/Logic


A very interesting result in this area -- in fact, a pretty
complete solution to the whole problem, it seems -- is in

A Proof-Carrying Authorization System. Lujo Bauer, Michael A. Schneider,
and Edward W. Felten. Technical report CS-TR-638-01, Department of
Computer Science, Princeton University, April 2001

 <- http://www.cs.princeton.edu/sip/projects/pca/

I'm trying to understand their work to see what it would take
to express their proofs in XML with URIs for terms and such.

The logic they use is pretty high powered; I wonder if we
could get by with less.

And I don't quite understand how they deal with quoting, or
if their solution to "Fred said X" actually involves quoting.

I wrote to them a while ago, I think, but I didn't get any reply.

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Monday, 28 April 2003 17:24:51 UTC