- From: Francois Bry <bry@ifi.lmu.de>
- Date: Thu, 11 May 2006 17:13:20 +0200
- To: W3C RIF WG <public-rif-wg@w3.org>
Bijan Parsia wrote: >>> and you'll see lots of people say >>> their theorem provers are sound and complete -- they are talking about >>> running code. > > This is a simple contraction for "my code, by and large, correctly > implements a sound and complete proof procedure". +1 François >> In the theorem proving community, sound is said of the theorem prover >> s.t. what it clainms to be logical consequences (dewfined in a model >> theory) actually are. Complete is used for a theorem prover that can >> compute all logical consequences. > > I wouldn't think so, at least not all the time, since I think a FOL > prover can be said to implement a complete procedure, but of course > it cannot compute all logical consequences. Sorry! I meant it in the sense of exhaustive: every logical consequwnce will come after some finite time. This is possible. > Soundness is about the relation between a proof theory and a > semantics, where, in general, the semantics are not proof theoretic. > I don't think that restricts you to model theoretic semantics -- > algebraic semantics could be fine. +1 > > Since we are trying to be a bit nice with our terminology, let me say > that it's not the happiest (even granting the possibility of > inferential *semantics* acknowledged; or, for example, in the case of > default logic, the lack of an *alternative* to a proof theoretic > characterization) to use the word "true" here. It's exactly the fact > that the derivations of a proof theory *might not be sound* that > helps differentiate semantics from proof theory. +1 > > There are definitely at least two notions of "semantics" floating > about: the first where the notion of meaning is connected to the > notion of truth, falsity, etc., and the other where the meaning of a > construct is connected to it's (computational) *behavior* (which may > connect back up to something more like the first). I don't want to > denigrate either approach (I *like* formal operational semantics for > programming languages), but if we are going to use semantics in this > ambiguous way, we should be extra careful with our use of certain > semantic terminology, e.g., truth. +1
Received on Thursday, 11 May 2006 15:13:24 UTC