From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Mon, 10 Nov 2003 18:52:41 -0500 (EST)

Message-Id: <20031110.185241.68553475.pfps@research.bell-labs.com>

To: connolly@w3.org

Cc: www-rdf-rules@w3.org

Date: Mon, 10 Nov 2003 18:52:41 -0500 (EST)

Message-Id: <20031110.185241.68553475.pfps@research.bell-labs.com>

To: connolly@w3.org

Cc: www-rdf-rules@w3.org

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 ResearchReceived on Monday, 10 November 2003 18:52:50 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:14 UTC
*