Re: "Axiomatic Semantics"

From: Sandro Hawke <sandro@w3.org>
Subject: "Axiomatic Semantics"
Date: Mon, 12 Aug 2002 10:44:45 -0400

> 
> Peter F. Patel-Schneider writes:
> > An axiomatization (not axiomatic semantics) of a language is a collection
> > of formulae in some logic that implements inference in the language, or, in
> > the case of DAML+OIL, that implements inference in a translation of the
> > language.  If the target logic has implemented reasoners, the
> > axiomatization can be used in these reasoners to create a reasoner for the
> > language.  Again, this reasoner will usually be ineffective unless care is
> > taken to write the axiomatization in a manner that exploits the strengths
> > of the target logic reasoner.
> ...
> > 3/ Axiomatizations can lead to trivial implementations of reasoners - just
> >    use a reasoner for the target logic.  However, the reasoner may not turn
> >    out to be effective.
> 
> Thanks for the wonderfully clear explanations!   There are two nits
> I'm hoping you can clear up:
> 
> 1.  Why do you dispute the phrase "axiomatic semantics"?  The first
> two pages of Google suggest the phrase is in common use (although only
> 20% as common as "axiomatization", but in fact "axiomatization" seems
> to have a wider range of meanings, perhaps because it's older).  I
> learned the phrase from DAML, heard it used at many DAML PI meetings,
> and until last week I never heard a complaint about it.

Well, an axiomatization does not, by itself, provide a semantics.  Instead
it depends on the semantics of the targe logic.  Also, ``axiomatic
semantics'' appears to be commonly used in the context of programming
languages, not logics.  So, I would prefer to not use this term for an
axiomatization of a logic, instead using ``axiomatization'', or maybe even
``translation plus axiomatization''.  

I was trying to separate axiomatizations from proof theories.  Of course,
an axiomatization leads to a proof theory if the target logic has a proof
theory, namely the proof theory consisting of first performing the
translation (if any) and then using the proof theory of the target logic,
augmenting any axioms of the target logic with the axiomatization of (the
translation of) the source logic.

> 2.  You say an axiomatization "implements inference", but wouldn't it
> be more accurate to say it describes or constrains inference?  As you
> say, it may lead "trivial implementations", but quite often it's not
> effective, and implementing is all about having practical effect.  I
> don't mean to be picking on your words; I just want to make sure I
> haven't misunderstood something here.

Hmm, yes, that might be a better way of saying it, particularly if the
axiomatization was not sound and complete.

> Thanks,
> 
>   -- sandro

peter

Received on Monday, 12 August 2002 11:05:23 UTC