Henson, (01)
I think we're converging. I appended a copy of your note below,
because it didn't get through the CL and Ontolog email handlers. (02)
> The suggestion of translating the partial functions into relations
> is actually the way that axiomatization of a topos as a first order
> theory was originally done. It works, but is messy but makes the
> logic embedding very remote from the mathematics. (03)
I agree. I give a similar explanation for using CGIF instead of CLIF
to represent and operate with graphs. They both have the same model
theory. But graph operations that are easy to state in CGIF are often
more complex in CLIF. (04)
> While the functions, such a composition and ordered pairs, are partial,
> they have simple definedness conditions which can easily be checked by
> a tool. One can just do the checks with an ordinary inference engine
> and carry on with the inference. (05)
An inference engine can unify two functional structures very simply.
But it would be harder to state the equivalent conditions on relational
structures and to implement them efficiently. (06)
> By extending/changing the semantics slightly one makes a much better
> convergence between logic and the mathematics done in the category
> theory way, than is done the way you suggested. (07)
Fundamental question: What do you mean by "extending/changing the
semantics slightly"? The model theory? Or the rules of inference? (08)
Many people (including me) consider rules of inference as implications
of the model theory. The choice of rules is a convenience (for human
factors or computational efficiency), not a change in semantics. (09)
For the CGIF <=> CLIF mapping, there is no change to the model theory,
but certain rules of inference, which are trivial to state in CGIF
cannot be stated in CLIF without a major increase in complexity.
See the excerpt below for the question by Larry Wos and the answer
in terms of Peirce's rules of inference. (010)
> If someone wanted to consider how to extend CL to accommodate this
> I would be very pleased for this to be a use case. (011)
I would recommend that as an important use case. Could you state
the definedness conditions and their implications -- preferably in CL
terms, rather than topos theory? (012)
John
______________________________________________________________________ (013)
Excerpt from http://www.jfsowa.com/pubs/semnet.htm (014)
Even today, Peirce’s rules provide insights that have eluded logicians
for many years. As an example, Larry Wos (1988) listed 33 unsolved
research problems in automated reasoning. Problem 24 asks about the
relationship between proofs using Gentzen’s rules for clauses and his
rules of natural deduction: (015)
"Is there a mapping between clause representation and natural-deduction
representation (and corresponding inference rules and strategies) that
causes reasoning programs based respectively on the two approaches or
paradigms to attack a given assignment in an essentially identical
fashion?" (016)
The answer follows from theorems that are easy to prove when stated in
existential graphs (Sowa 2011, Section 6): (017)
1. Any proof by Gentzen’s system of natural deduction can be converted
automatically to a proof by Peirce’s rules. The converse is not true,
because certain proofs by Peirce’s rules can be significantly faster
than proofs by Gentzen’s rules (Dau 2006). (018)
2. Any proof derived by a resolution theorem prover in clause form can
be converted to a proof using Peirce’s rules by negating each step,
reversing the order, and writing each step as an existential graph. (019)
To answer Wos, proofs in either of Gentzen’s systems can be translated,
step by step, to an equivalent EG proof. Some, but not all, can be
translated from EGs to a proof in the other system by Gentzen. Peirce’s
framework is a generalization that subsumes both. (020)
References: (021)
Dau, Frithjof (2006). Some notes on proofs with Alpha graphs. In
Conceptual Structures: Inspiration and Application, (LNAI 4068), H.
Schärfe, P. Hitzler, and P. Øhrstrom (eds.), Berlin: Springer. pp. 172-188. (022)
Sowa, John F. (2011) Peirce’s tutorial on existential graphs, Semiotica
186:1-4, 345-394. http://www.jfsowa.com/pubs/egtut.pdf (023)
Wos, Larry (1988) Automated Reasoning: 33 Basic Research Problems,
Englewood Cliffs, NJ: Prentice Hall. (024)
-------- Original Message --------
Subject: Re: Giving SysML a formal semantics
Date: Mon, 7 Oct 2013 08:14:57 -0500
From: Henson Graves (025)
John, (026)
The suggestion of translating the partial functions into relations is
actually the way that axiomatization of a topos as a first order theory was
originally done. It works, but is messy but makes the logic embedding very
remote from the mathematics. Proofs in the logic would not resemble what an
informal argument would look like and it would be very hard to translate
the
other way. (027)
While the functions, such a composition and ordered pairs, are partial,
they
have simple definedness conditions which can easily be checked by a tool.
one can just do the checks with an ordinary inference engine and carry on
with the inference. This situation is not like general partial recursively
enumerable functions. By extending/changing the semantics slightly one
makes
a much better convergence between logic and the mathematics done in the
category theory way, than is done the way you suggested. Don't
misunderstand, your suggestion was what was originally done which had
enormous positive consequences. But I believe the partial function approach
has many practical advantages, is sound from the logic viewpoint, and makes
even more sense when you look at embedding engineering models in logic.
There is of course much more to say technically to advocate this. (028)
If someone wanted to consider how to extend CL to accommodate this I would
be very pleased for this to be a use case. I suspect almost nothing would
have to be changed in an inference engine, only the user's manual would
have
to be changed a bit. (029)
Henson (030)
_________________________________________________________________
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 (031)
|