Dear Nicolas, (01)
<<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: (02)
http://www.cse.ucsd.edu/users/goguen/projs/inst.html (03)
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. (04)
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). (05)
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. (06)
However, to do this constrcution, or to perform the mapping as you wrote: (07)
"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) (08)
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. (09)
Thanks, (010)
Arun (011)
Nicolas F Rouquette wrote: (012)
> 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
>
>
> (013)
_________________________________________________________________
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 (014)
|