Re: soundness for RIF

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