Re: Rules WG -- draft charter

From: Dan Connolly <connolly@w3.org>
Subject: Re: Rules WG -- draft charter
Date: Mon, 10 Nov 2003 16:28:50 -0600

[...]

> > The document appears to require that rules be equivalent to material
> > implications, which is not their treatment in many rule systems.  In
> > particular, in some rule formulations that allow disjunctive information
> > rules with false consequents are not equivalent to classical negation.
> 
> I don't follow. Perhaps you could elaborate with an example?

From 

a v b
a -> false 
b -> false

is not possible to derive a contradiction in some rule formalisms

[...]

> > It is not the case that proof checking is ``computationally much easier
> > than theorem proving''.
> 
> Yes, it is, in at least a few interesting cases:
> 
>   This makes the AF logic unsuitable for use in traditional distributed
>   authentication frameworks in which the server is given a set of credentials
>   and must decide whether to grant access. This problem can be avoided in
>   the server by making it the client's responsibility to generate proofs.
>   The server must now only check that the proof is valid -- this is not
>   difficult even in an undecidable logic.
>   
> [Bauer2002] A General and Flexible Access-Control System for the Web.
> Lujo Bauer, Michael A. Schneider, and Edward W. Felten. To appear in
> Proceedings of the 11th USENIX Security Symposium, August 2002.
> among Proof-Carrying Authorization papers
> http://www.cs.princeton.edu/sip/projects/pca/

This statement is not true in general, if only because a proof may be too
long to be practical to transmit.

> "Proofs found by programs are always questionable. Our approach to this
> problem is to have the theorem prover construct a detailed proof object
> and have a very simple program (written in a high-level language) check
> that the proof object is correct. The proof checking program is simple
> enough that it can be scrutinized by humans, and formal
> verification is probably feasible. [...] "
>   -- http://www-unix.mcs.anl.gov/~mccune/papers/robbins/

This again depends on the logic in question.  In a non-monotonic logic
proof checking a single, atomic step of the proof may be intractable or
undecidable, as it may depend on the unprovability of a particular fact.

> >  In decidable logics the length of a proof may
> > be similar to the number of computational steps required to proove a
> > particular result.  This may lead to a PSPACE deduction procedure but proof
> > checking requiring exponential space just to store the proof.
> 
> I can see a few options for cases like that...
> 
>   * don't do that

Well, sometimes you just have to.  How else are you going to check an
exponentially-long proof?

>   * treat such steps as a built-in, like floating point multiplication

Ah yes, but then a single proof checking step may take an exponentially
long amount of time.

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

It is generally the case that proof checking is no harder than proving,
although I don't remember a proof to this effect.  :-)

It is certainly the case that proof checking is usually easier than
proving, and mostly proof checking is very much easier than proving, but
this is certainly not always the case.

Peter F. Patel-Schneider
Bell Labs Research

Received on Monday, 10 November 2003 18:52:50 UTC