- From: Bijan Parsia <bparsia@isr.umd.edu>
- Date: Thu, 11 May 2006 13:23:43 +0100
- To: Francois Bry <bry@ifi.lmu.de>
- Cc: W3C RIF WG <public-rif-wg@w3.org>
On May 10, 2006, at 12:30 PM, Francois Bry wrote: > Sandro Hawke wrote: [snip] >> >> Really? I often hear the term "sound" used somewhat more loosely to No need to perpetuate slop in a context where precise communication is very highly desirable. [snip] >> Google for "sound" "theorem prover" Google for "sound foundation" and you'll see lots of people say that stone construction leads to sound foundations. And if you google for "sound system" you'll see lots of people say that their sound system has high fidelity. So? >> 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". (Frankly, this appeal to google is absurd and, in my opinion, counterproductive. It is *crazy* to try to fly in face the plain and well understood central meaning of a term with regard to a particular subject matter by appeal to general and loose talk, especially when said term has a *precise* formal definition. It's even crazier to do so by appeal to the thinnest of empirical linguistic evidence. What purpose does this serve?) > 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. > When used in this community fdor > software, it is always used that way. (I am very, very sure of what > I say). >> While I know OWL has a model theory, you're claiming that these >> theorem >> provers must be for logics with model theories because they are >> claiming >> soundness? 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. > I am saying that usually in logic the concept of soundness is used > as I > said. I am not excluding it being used by some logicians in another > way > but this would be quite unusual. >> Or dictionaries: >> >> sound / unsound >> >> Distinction among deductive arguments. A sound argument both has >> true premises and employs a valid inference; its conclusion must >> therefore be true. > This is exactly what I said. In logics there are two ways to define > true 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. 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. [snip] Cheers, Bijan.
Received on Thursday, 11 May 2006 12:23:42 UTC