Re: [ontolog-forum] Role of definitions (Remember the poor human)

["Adrian Walker" <adriandwalker@xxxxxxxxx>]

Hi Chris --

[Adrian]
>   * Semantics2   Specifies what inferences should be made from
> any collection of rules and facts -- usually based on a model
> theory, e.g. as in [3].

[Chris]
That's what is usually called *proof theory* in logic.  As you note,
a proof theory is indeed typically *based on* a model theory, but the
whole point of soundness and completeness theorems in logic is
precisely to prove that the inferences that can be made from a
collection of assumptions ("facts") according to a proof theory
("rules" (roughly)) are in fact sanctioned by the model theory
(a.k.a., the formal semantics) given for the language of the proof
theory.  It seems to me to be very unwise (and certainly not in
keeping with standard terminology in mathematical logic) to call
proof theory a sort of semantics

[Adrian]  I think if you read the following again

>   * Semantics2   Specifies what an inferences should be made from
> any collection of rules and facts -- usually based on a model
> theory, e.g. as in [3].

(and if you have time to look at the paper), you'll see that we are in complete agreement.  

The essential point is to have a model 
theory as a gold standard to which programmers must adhere when implementing an engine.

                                     Cheers, -- Adrian

[3]  Backchain Iteration: Towards a Practical Inference Method that is Simple 
  Enough to be Proved Terminating, Sound and Complete. Journal of Automated Reasoning, 11:1-22

On 2/13/07, Christopher Menzel < cmenzel@xxxxxxxx> wrote:

On Feb 13, 2007, at 11:11 AM, Adrian Walker wrote:
> Barry wrote...
>
>> From my experience working with biologists and medical researchers
>> on ontologies, definitions (ideally both natural language definitions
>> and equivalent formal definitions) play a very useful role when it
>> comes to ensuring that ontologies are populated in consistent ways
>> across disciplines and subsequently used correctly (or indeed at all)
>> in practical applications. Most of those involved in such use will
>> not have logical or computer science expertise. Where else should
>> they turn to find out what a term means?
>
> It may actually be useful to expand Barry's observation, and also
> W3C-style "semantics" as follows:
>
>   * Semantics1   Is (meta)data semantics, W3C-style
>
>   * Semantics2   Specifies what an inferences should be made from
> any collection of rules and facts -- usually based on a model
> theory, e.g. as in [3].

That's what is usually called *proof theory* in logic.  As you note,
a proof theory is indeed typically *based on* a model theory, but the
whole point of soundness and completeness theorems in logic is
precisely to prove that the inferences that can be made from a
collection of assumptions ("facts") according to a proof theory
("rules" (roughly)) are in fact sanctioned by the model theory
(a.k.a., the formal semantics) given for the language of the proof
theory.  It seems to me to be very unwise (and certainly not in
keeping with standard terminology in mathematical logic) to call
proof theory a sort of semantics, as it runs together concepts that
logicians have with great care and for good reason have cleanly
separated.

If it has become the practice to use "semantics" as a synonym for the
underlying proof theory of a system in some circles, it is
unfortunate.  Ideally, it would be good to change this behavior, as
it can lead to confusion, but I don't know of the extent of practice,
so don't know if that is a realistic expectation.

Chris Menzel


_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto: ontolog-forum@xxxxxxxxxxxxxxxx

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (01)