Yes, almost by definition you will not have much published research in the
model-theoretic implications of procedural attachment, I think. There is
limited research in general for denotational semantics of procedural
programming. I think you would have to first formulate your procedural language
into a declarative language/logic, perhaps a functional programming language.
However, mathematical theories, "little theories", ala Bill Farmer's work (he's
at McMaster U, CA, I think) may help. Or you might think about SMT,
Satisfiability Modulo Theory, reasoners, which are SAT reasoners that bring in
theories such as reals, bit vectors, etc. They are kind of constraint logic
programming systems. (01)
I also vaguely remember Hoare logic from my formal methods days, that tried to
formalize some procedural programming constructs. (02)
Thanks,
Leo (03)
>-----Original Message-----
>From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-
>bounces@xxxxxxxxxxxxxxxx] On Behalf Of John F Sowa
>Sent: Saturday, December 08, 2012 10:18 AM
>To: ontolog-forum@xxxxxxxxxxxxxxxx
>Subject: Re: [ontolog-forum] Hybrid Reasoning Literature / Systems / Model
>Theory
>
>Ali,
>
>I just wanted to comment on the following point:
>
>> It's been difficult to find papers which discus the model theoretic
>> implications of I guess what amounts to procedural attachment.
>
>The term "procedural attachment" was usually used by the "scruffies",
>who avoid formal methods. The "neats" were very critical of that
>work. So none of them would use that term in theoretical papers.
>
>My recommendation for handling procedures in a formal way is to
>look at the literature on formal specifications of software.
>They specify each procedure by its preconditions and postconditions.
>
>On the procedural side, any kind of scruffy code is permitted,
>as long as it is constrained by the preconditions at the beginning
>and the postconditions at the end. In between, all bets are off.
>
>Mathematica is probably the most extensive practical development
>of these techniques. They use formal axioms, do symbolic reasoning,
>and keep track of the preconditions and postconditions.
>
>But when you need efficient code, Mathematica will compile the
>specifications into executable programs in FORTRAN or C.
>
>John
>
>___________________________________________________________
>______
>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
> (04)
_________________________________________________________________
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 (05)
|