[with corrected email address] (01)
Fabian, (02)
[I add the CL list to the cc since this is relevant for CL] (03)
after re-thinking this issue, my suggestion to resolve it is as follows: (04)
1.
the notion of reduct for Common Logic is defined in the following way: a
Common Logic model $I$ is reduced to a smaller signature by
a) restricting the interpretation function int_I to the smaller signature
b) removing all elements of the universe of reference satsifying all the
following conditions:
- they are not in the universe of discourse,
- they are the interpretation of a non-discourse name in I,
- they are not the interpretation of a non-discourse name in I
restricted to the smaller signature. (05)
With this notion of reduct, definitions in segregated dialects of Common
Logic are indeed both definitional and conservative extensions in the
sense of the OntoIOp terminology: (06)
An extension O2 of an ontology O1 is a *conservative extension*, if each
model of O1 can be *expanded* to a model of O2.
An extension O2 of an ontology O1 is a *definitional extensionAn
extension O2 of an ontology O1 is a *definitional extension*, if each
model of O1 can be *uniquely expanded* to a model of O2. (07)
Note that model expansions in segregated dialects simply can add new
elements to the universe of reference, which are then used to denote the
newly defined functions and predicates. (08)
However, this solution does not work for non-segregated dialectcs,
because they do not make use of non-discourse names (and throwing out
elements from the universe of discourse is problematic, because then
satisfaction would no longer be invariant under reduct). (09)
2.
The following notion is added: (010)
An extension O2 of an ontology O1 is a *weak definitional extension*, if
each model of O1 can be *expanded to at most one* model of O2.
(This means that an extension if definitional iff it is both
conservative and weakly definitional.) (011)
With this terminology, most most definition-like looking extensions in
non-segregated dialects of Common Logic would be weak definitional
extensions, but not definitional nor conservative. Lack of
conservativity is due the fact that these extensions lead to new
theorems in the unextended language stating the existence of the newly
defined objects. And I cannot see a meaningful way of calling this
"conservative" or "definitional", because the theory is changed.
(Note that higher-order logic with Henkin semantics does not suffer from
this problem, because lambda-terms guarantee the existence of all
explicitly definable objects.) (012)
All the best,
Till (013)
Am 06.06.2012 14:19, schrieb Fabian Neuhaus:
>
>
> Till,
> I understand that the definition works well for many logics. My point is that
>since CL is one of the two major ontology languages, and CLIF plays a
>particular role in the standard because one of the semantics of DOL is defined
>in terms of translations into CLIF, we should try to make it work for CLIF.
>
> I am not sure whether extensionality vs. intensionality is the only issue.
>Let's consider an example which contains an extensionality axiom explicitly.
>
> Let's assume O_1 =
> (forall (x y) (if (R x y) (R y x)))
>
> (forall (?R1 ?R2 ...s)
> (if
> (iff (?R1 ...s) (?R2 ...s))
> (= ?R1 ?R2)
> ))
>
> Let's assume O_2 =
> import O_1
> (forall (...s) (iff (S ...s) (not (R ...s))))
>
> Consider model A
> Universe = {1, 2}
> Ext(1) = {}
> Ext(2) = {1}
> I(R) = 1
>
> Model A is a model of O_1. Thus, there are no-coextensional entities in the
>domain. If "expansion" is defined in the way that I understand it (namely that
>it does not change the universe), there are two possible expansions of A:
>
> B
> Universe = {1, 2}
> Ext(1) = {}
> Ext(2) = {1}
> I(R) = 1
> I(S) = 1
>
> C
> Universe = {1, 2}
> Ext(1) = {}
> Ext(2) = {1}
> I(R) = 1
> I(S) = 2
>
>
> Both B and C are not models of O_2. Hence, O_2 is not a definitorial
>extension of O_1 according to the definition. Thus, if I understand
>"expansion" correctly, this example works regardless of the assumption about
>extensionality of relations.
>
> I guess, the question is how do we define "expansion" for CL?
>
> Best
> Fabian
>
>
>
>
>
>
> On Jun 5, 2012, at 6:39 PM, Till Mossakowski wrote:
>
>> Dear Fabian,
>>
>> this is an interesting point, thanks for raising it.
>> Note that the notion of definitional extension on page 9 works well for
>> many logics.
>> Concerning Common Logic, I am not entirely sure. Would you intuitively
>> call O_2 a definitional extension of O_1 even when facing the fact there
>> are two different (though "extensionally" equivalent) extensions of the
>> O_1-model A two an O_2-model?
>> It seems to me that since predicates in Common Logic has a more
>> intensional flavour, a predicate is not fully defined by just specifying
>> its extension...
>>
>> Best, Till
>>
>> Am 05.06.2012 19:49, schrieb Fabian Neuhaus:
>>> All,
>>> When I changed the models to improve readability, I introduced more
>>> entities -- which lead to a minor error. This is the corrected version.
>>> Sorry about that.
>>> Fabian
>>>
>>> *From: *Fabian Neuhaus<fneuhaus@xxxxxxxx<mailto:fneuhaus@xxxxxxxx>>
>>> *Date: *June 5, 2012 1:03:38 PM EDT
>>> *To: *"OntoIOp WG Discussion (co)"<ontoiop-wg@xxxxxxxxxxxxxxxx
>>> <mailto:ontoiop-wg@xxxxxxxxxxxxxxxx>>
>>> *Subject: **[ontoiop-wg] definitorial extensions in CL*
>>> *Reply-To: *"OntoIOp WG Discussion (co)"<ontoiop-wg@xxxxxxxxxxxxxxxx
>>> <mailto:ontoiop-wg@xxxxxxxxxxxxxxxx>>
>>>
>>> All,
>>> I am looking at the definition of definitorial extension on page 9. How
>>> does this work for unsegregated CL dialects like CLIF?
>>>
>>> Let's assume O_1 =
>>> (forall (x y) (if (R x y) (R y x)))
>>>
>>> Let's assume O_2 =
>>> import O_1
>>> (forall (x y) (iff (S x y) (not (R y x))))
>>>
>>> Intuitively, O_2 is a definitorial extension of O_1, because S is
>>> defined in terms of R.
>>> According to the definition, a O_2 is a definitorial extension of O_1 if
>>> each model of O_1 can be uniquely expanded to a model of O_2 . I assume
>>> that means (a) there is an expansion and (b) there is only one.
>>>
>>> Consider the O_1 model A and the O_2 models B and C below. (I ignore the
>>> interpretation of names as functions, since it is not relevant to the
>>> argument.) It seems to me that B and C are both expansions of A. Hence,
>>> O_2 is -- according to the definition -- not a definitorial extension of
>>> O_1. Which either means that the definition is wrong or that there will
>>> be very few definitorial extensions of CLIF ontologies.
>>>
>>> Best
>>> Fabian
>>>
>>> A
>>> Universe = {1, 2, 3, 4}
>>> Ext(1) = {}
>>> Ext(2) = {(1,1) (1,2) (1,3), ..., (4,4) }
>>> Ext(3) = {(1,1) (1,2) (1,3), ..., (4,4) }
>>> Ext(4) = {2}
>>> I(R) = 1
>>>
>>> B
>>> Universe = {1, 2, 3, 4}
>>> Ext(1) = {}
>>> Ext(2) = {(1,1) (1,2) (1,3), ..., (4,4)}
>>> Ext(3) = {(1,1) (1,2) (1,3), ..., (4,4)}
>>> Ext(4) = {2}
>>> I(R) = 1
>>> I(S) = 2
>>>
>>> C
>>> Universe = {1, 2, 3, 4}
>>> Ext(1) = {}
>>> Ext(2) = {(1,1) (1,2) (1,3), ..., (4,4) }
>>> Ext(3) = {(1,1) (1,2) (1,3), ..., (4,4) }
>>> Ext(4) = {2}
>>> I(R) = 1
>>> I(S) = 3
>>>
>>>
>>>
>>>
>>>
>>>>
>>>>
>>>>
>>>> _________________________________________________________________
>>>> To Post: mailto:ontoiop-wg@xxxxxxxxxxxxxxxx
>>>> Msg Archives: http://interop.cim3.net/forum/ontoiop-wg/
>>>> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
>>>> Community Files (co): http://interop.cim3.net/file/work/OntoIOp/
>>>> Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OntoIOp
>>>> Community Portal: http://bit.ly/ISO-TC37-SC3-OntoIOp
>>>>
>>>
>>>
>>>
>>>
>>> _________________________________________________________________
>>> To Post: mailto:ontoiop-wg@xxxxxxxxxxxxxxxx
>>> Msg Archives: http://interop.cim3.net/forum/ontoiop-wg/
>>> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
>>> Community Files (co): http://interop.cim3.net/file/work/OntoIOp/
>>> Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OntoIOp
>>> Community Portal: http://bit.ly/ISO-TC37-SC3-OntoIOp
>>>
>>
>>
>> --
>> Prof. Dr. Till Mossakowski Cartesium, room 2.51 Phone +49-421-218-64226
>> DFKI GmbH Bremen Fax +49-421-218-9864226
>> Cyber-Physical Systems Till.Mossakowski@xxxxxxx
>> Enrique-Schmidt-Str. 5, D-28359 Bremen
>> http://www.informatik.uni-bremen.de/~till/
>>
>> Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
>> principal office, *not* the address for mail etc.!!!:
>> Trippstadter Str. 122, D-67663 Kaiserslautern
>> management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff
>> supervisory board: Prof. Hans A. Aukes (chair)
>> Amtsgericht Kaiserslautern, HRB 2313
>>
>> _________________________________________________________________
>> To Post: mailto:ontoiop-wg@xxxxxxxxxxxxxxxx
>> Msg Archives: http://interop.cim3.net/forum/ontoiop-wg/
>> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
>> Community Files (co): http://interop.cim3.net/file/work/OntoIOp/
>> Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OntoIOp
>> Community Portal: http://bit.ly/ISO-TC37-SC3-OntoIOp
>>
>
>
> _________________________________________________________________
> To Post: mailto:ontoiop-wg@xxxxxxxxxxxxxxxx
> Msg Archives: http://interop.cim3.net/forum/ontoiop-wg/
> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
> Community Files (co): http://interop.cim3.net/file/work/OntoIOp/
> Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OntoIOp
> Community Portal: http://bit.ly/ISO-TC37-SC3-OntoIOp
> (014)
--
Prof. Dr. Till Mossakowski Cartesium, room 2.51 Phone +49-421-218-64226
DFKI GmbH Bremen Fax +49-421-218-9864226
Cyber-Physical Systems Till.Mossakowski@xxxxxxx
Enrique-Schmidt-Str. 5, D-28359 Bremen
http://www.informatik.uni-bremen.de/~till/ (015)
Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
principal office, *not* the address for mail etc.!!!:
Trippstadter Str. 122, D-67663 Kaiserslautern
management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff
supervisory board: Prof. Hans A. Aukes (chair)
Amtsgericht Kaiserslautern, HRB 2313 (016)
_________________________________________________________________
To Post: mailto:ontoiop-forum@xxxxxxxxxxxxxxxx
Message Archives: http://ontolog.cim3.net/forum/ontoiop-forum/
Config/Unsubscribe: http://ontolog.cim3.net/mailman/listinfo/ontoiop-forum/
Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
Community Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OntoIOp (017)
|