Dear Nicolas, (01)
As a further update, the other notion I am looking at is how systems can
negotiate an understanding at runtime that would preclude a-priori
encoding of the transformations as indicated. (02)
The second intended update is that we use our new ontology (of whatever
it looks like) to apply models of analogical/cognitive reasoning
strategies that employ the various provers or modules or other methods
in a "network of conversations" to accomplish interoperability in the
large. This necessarily rules out having a legislated single model but
rather interconnected models forming a system such the models that
evolve denser interconnections would naturally indicate generality or
applicability to world at large whilst those whos interconnections
deteriorate or ar sparse wouild indicate highly specialised domains.
This comment in and of itself would reuqire operatiions over the
model-network layer and that means we need an ontology for the
metatheoretic *aspects* (aspects like isomorphisms, mappings,
coordination etc...) (03)
Thanks, (04)
Arun (05)
Arun Majumdar wrote: (06)
> Dear Nicolas,
>
> <<Is this the kind of approach that you are advocating Arun? >> This
> is roughly it - between these various systems, I have not seen a
> ontological effort to provide the structure that we can share and
> use. Perhaps we can consider an approach using these specifications
> as objects in an ontology, upon which rules as morphisms (also entered
> as objects in the ontology) that provides a way to interoperate any
> logics/theory/model combinations. I have suggested that we look to
> Category Theory and to Goguen's Institutions in particular as a
> starting point:
>
> http://www.cse.ucsd.edu/users/goguen/projs/inst.html
>
> Hence, very roughly, any real-world example as you have kindly
> provided, suggests we need a (controlled vocabulary) language to talk
> about the collection of objects that describe theories belonging to a
> Category of logics in which those theories are valid and that those
> morphisms become the objects as well etc.,.. so hence my pointer to
> instiutions: it means that systems that intend to interoperate, set
> up "header" that up front provides their operational semantics in
> terms of these mappings,. which could be written in Common Logic.
> So the general idea I am thinking about is of building an onotlogy of
> different logics as an ontology whose language is spoken from Category
> Theory but that relates directly to systems like Specware etc... using
> Common Logic to build with (but not from an concept-definition
> word-meaning view as per my note regarding Kuhn).
>
> For example, consider mapping or interoperting between a logic of
> practical reasoning { like G. H. von Wright, /Practical inference/,
> The Philosophical Review *72* (1963), 159-179. } and a linear logic
> {like Jean Yves Girard, Theoretical Computer Science archive Volume
> 50, Issue 1, Jan. 1987} and Petri Nets { Carl Adam Petri,
> /Kommunikation mit Automaten, University Of Bohn, 1962/}. One
> possible suggestion is they can be made isomorphic to Petri Nets where
> the operational semantics of Petri nets (ie. the transitions) are
> written down as equivalencies to the proof procedures of Linear Logic
> whose semantics stem from other counterfactual or practical reasoning
> frameworks as mentioned.
> However, to do this constrcution, or to perform the mapping as you
> wrote:
>
> "mapped via isomorphism to a *semantically equivalent form* in another
> language for which we have a decision procedure or theorem prover" (I
> added the emphasis)
>
> suggests that an ontology be written for this purpose (which if used
> by systems may be extremely useful in cases where the interchange of
> knowledge, for example, using IKL from IKRIS (when ready) changes the
> state of knowledge being interoperated upon as what happens between
> people in a discussion group, or social agents in a computer as a
> sommunicating system). So semantically equivalent could refer to,
> for example, structural or behavioral equivalencies (in the sense of
> bisimulations) where different systems could interoperate at either or
> in between those views.
>
> Thanks,
>
> Arun
>
> Nicolas F Rouquette wrote:
>
>> Arun, Chris:
>>
>> In SpecWare (http://www.specware.org), there is one often used
>> technique that resembles the kind of metatheory you are talking about.
>> The principle is, roughly, to write a small specification that
>> provides an axiomatic theory of something; e.g., the concept of list,
>> set, array, etc...
>> and such specifications are used as "metatheories" by specifying
>> axioms regarding the existence of an isomorphism
>> between the "metatheory" specification (e.g., list, set, ...) to the
>> target "theory" which we claim to have the properties of the metatheory.
>>
>> I believe that other systems like HetCASL (see:
>> http://www.brics.dk/Projects/CoFI/) do similar tricks.
>> The key point; however, is that the "metatheory" and "theory" are
>> written in the same "logic" which, if it isn't implemented "natively"
>> can also be mapped via isomorphism to a semantically equivalent form
>> in another language for which we have a decision procedure
>> or theorem prover (e.g., SpecWare encodes its "MetaSlang" logic into
>> SNARK's language at which point it can use SNARK's theorem prover
>> to reason (indirectly) about logic sentences in MetaSlang).
>>
>> Is this the kind of approach that you are advocating Arun?
>>
>> -- Nicolas.
>>
>> Arun Majumdar wrote:
>>
>>> Dear Chris,
>>>
>>> Yes - that is precisely it! And then I was indicating my interest to
>>> enrich this with by building in a model for Category Theory (ie. to
>>> create a version with rules and operations) as a second step.
>>>
>>> Let me see if I can refine my language on this (noting that my
>>> curiosity and interest stem from the analogical cognitive reasoning
>>> capabilities that I naturally perceive humans to perform without
>>> even thinking about it!)
>>>
>>> I am trying to identify a logic using CL that would contain
>>> propositional connectives, or modifiers whose semantics refers to
>>> other models external to the model upon which they are defined. I
>>> think I can call this the metalogical operators that permit CL to be
>>> interpreted dynamically, so that CL might be used to provide a
>>> language to transform/change/update the current model (even CL
>>> itself). These metalogical (extralogical?) operatorssuggest that we
>>> try to capture the properties of model in an indirect manner by
>>> parameters of the model’s possible modifications.
>>>
>>> My hope is that we can consider for further use what elements along
>>> the lines suggested might provide a dynamical, evolvable,
>>> model-theoretic semantics, in which Kripkean possible-world
>>> semantics applies to levels of models (in a single state that
>>> perhaps we might over-zealously call 'context'?) instead of the
>>> level of states in a single model.
>>>
>>> Is there a preffered pointer to the Common Logic material regarding
>>> the proposals you mentioned (as I went to the site but was unsure
>>> and hope that you have indications where specifically I might look) ?
>>>
>>> Thank you Chris,
>>>
>>> Arun
>>>
>>> Chris Menzel wrote:
>>>
>>>> First, I kvetch yet again: Can we not have a COSMO-WG mailing list
>>>> rather than a humongous cc list?
>>>>
>>>> On Wed, Jan 18, 2006 at 12:29:21AM -0500, Arun Majumdar wrote:
>>>>
>>>>
>>>>> Dear Leo,
>>>>>
>>>>> You wrote the following (to which I strongly agree and have some
>>>>> comments following)
>>>>>
>>>>>
>>>>>
>>>>>> I would use some variant of Common Logic (and possibly IKL from the
>>>>>> IKRIS project, once that is fully specified), because it (they) as
>>>>>> first-order logic languages are more expressive formally than
>>>>>> >OWL+SWRL.
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>> In my current commercial work elsewhere, the most troublesome
>>>>> aspect that I face in interoperability projects is the difficulty
>>>>> defining a theory that directly supports a first-order
>>>>> manipulation of theories and models, independently from the
>>>>> particular foundational ontology that it is plugged in: Common
>>>>> Logic is an excellent first step, however, all ACL's for
>>>>> knowledge exchange require the latter (theory) to succeed
>>>>> ...
>>>>>
>>>>
>>>>
>>>>
>>>>
>>>> Let me just see if I understand you, Arun: You want a formal
>>>> first-order theory that, in essence, axiomatizes the metatheory --
>>>> notably, the proof theory and the model theory -- of first-order
>>>> logic.
>>>> So, more specifically, you want a theory that axiomatizes such
>>>> predicates as "constant", "predicate", "formula", "proof",
>>>> "interpretation", "true in an interpretation", etc, is that right? Of
>>>> course, through the magic of encoding, we already *have* such a theory
>>>> -- Zermelo-Fraenkel set theory -- but I take it you'd prefer
>>>> something a
>>>> bit less abstract. The Common Logic group has already come up with a
>>>> couple of proposals for theories of quotation that enable one to
>>>> introduce metatheoretic predicates like the ones above. Add enough
>>>> set
>>>> theory to define the semantic predicates, and the result would seem to
>>>> be the sort of thing you are looking for.
>>>>
>>>> Chris Menzel
>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>>>
>>> _________________________________________________________________
>>> Message Archives: http://colab.cim3.net/forum/ontac-dev/
>>> To Post: mailto:ontac-dev@xxxxxxxxxxxxxx
>>> Subscribe/Unsubscribe/Config:
>>> http://colab.cim3.net/mailman/listinfo/ontac-dev/
>>> Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
>>> Community Wiki:
>>> http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG
>>>
>>>
>>
>>
>> _________________________________________________________________
>> Message Archives: http://colab.cim3.net/forum/ontac-dev/
>> To Post: mailto:ontac-dev@xxxxxxxxxxxxxx
>> Subscribe/Unsubscribe/Config:
>> http://colab.cim3.net/mailman/listinfo/ontac-dev/
>> Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
>> Community Wiki:
>> http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG
>>
>>
>>
>
>
> _________________________________________________________________
> Message Archives: http://colab.cim3.net/forum/ontac-dev/
> To Post: mailto:ontac-dev@xxxxxxxxxxxxxx
> Subscribe/Unsubscribe/Config:
> http://colab.cim3.net/mailman/listinfo/ontac-dev/
> Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
> Community Wiki:
> http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG
>
>
> (07)
_________________________________________________________________
Message Archives: http://colab.cim3.net/forum/ontac-dev/
To Post: mailto:ontac-dev@xxxxxxxxxxxxxx
Subscribe/Unsubscribe/Config: http://colab.cim3.net/mailman/listinfo/ontac-dev/
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki:
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG (08)
|