Henson, (01)
I completely agree with your summary (copy below), and I have always
believed that sorted logics have some important advantages. That's
the major reason why I have strongly encouraged the use of restricted
quantifiers in Common Logic to represent sorts in other logics. (02)
But there are two important issues: (03)
1. Your article [1] discussed the many reasons why any specification
language must itself have a formal specification. But it didn't
mention the fUML work [2] on specifying UML & SysML. (04)
2. I didn't attempt a complete translation of that article to
Common Logic, but I didn't see any ABD statement that could not
be translated to an equivalent CL statement. Why not adopt CL
model theory as the semantic foundation? (05)
> There is one difference from standard FOL practice. The first order
> operations are partial, but have definedness conditions expressed
> in the logic. (06)
Partial functions have been discussed on the CL list. One way of
handling them is to use the IEEE convention of assigning special
values such as NotANumber (NaN). You can also use quantifier
restrictions to ensure that variables stay within the domain. (07)
> This topos ontology approach enables a lot of statements that are
> higher order in some formalisms to be first order. (08)
That's good. CL has a first-order model theory and proof theory.
But it also supports quantifiers over functions and relations.
You could specify the topos ontology in CL and show how to
translate every ABD statement to an equivalent CL statement. (09)
That approach would enable you to build on and improve the current
fUML work instead of replacing it with something totally different.
It would also enable you to form an alliance with the fUML developers
instead of competing with them. (010)
John (011)
References: (012)
1.
http://www.omgwiki.org/MBSE/lib/exe/fetch.php?media=mbse:10.1007_s10472-011-9267-5.pdf (013)
2. Executable UML/SysML Semantics Project Report (Final), November 2008
To get report, type "xuml sysml fuml" to Google (without quotes). (014)
-------- Original Message --------
Subject: Re: Giving SysML a formal semantics
Date: Sun, 6 Oct 2013 09:19:46 -0500
From: Henson Graves (015)
John, (016)
ABD logic is actually an axiomatization of the map and type (object)
constructions of topos theory in a first order two sorted language. The
sorts are map and type. (017)
There is one difference from standard FOL practice. The first order
operations are partial, but have definedness conditions expressed
in the logic. There are of course FOL systems that admit this. For
example, composition of maps is a first order function symbol, but is
defined only when the appropriate domains and ranges match for the maps
being composed. (018)
What one is doing is not denying FOL its proper place in the sun,
but simply using FOL with definedness conditions for operations and
predicates, and with a specific ontology, based on topos theory, which
has been proven to be sufficient to do a lot of mathematics and science
in. This topos ontology approach enables a lot of statements that are
higher order in some formalisms to be first order. (019)
Henson (020)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (021)
|