"Axiomatic Semantics"

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.

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.

Thanks,

  -- sandro

Received on Monday, 12 August 2002 10:48:00 UTC