JAIST Repository: Theorem Proving and Institutions
3
0
0
全文
(2) Theorem Proving and Institutions. by. Daniel GAINA. submitted to Japan Advanced Institute of Science and Technology in partial fulfillment of the requirements for the degree of Doctor of Philosophy. Supervisor: Professor Kokichi FUTATSUGI. School of Information Science Japan Advanced Institute of Science and Technology. September 24, 2009.
(3) Abstract We investigate proof rules in various logics used in the area of computer science and prove their soundness and completeness in the abstract framework of institutions. The soundness and completeness results have great significance for logics because they establish a correspondence between the semantic truth and (syntactic) provability. We also specify and verify the correctness of software systems showing how theoretical results may be used in concrete specification examples. During the process of software specification, we often use different logical systems to capture particular aspects of software systems. Each part of a software system may be described by a distinct logical system that best fit considered problems. It is important to present a (abstract) formal concept of a logical system which covers the population explosion of logics used in computer science. Institution theory of Goguen and Burstall arouse out of this necessity, with the ambition of doing as much as possible at a level of abstraction, independent of any particular logic. We try to provide general ideas and results that can be easily applied to a multitude of logical systems and may be reused in different contexts. This research is largely focused on foundational aspects but it also takes seriously the task of providing support for the specification and verification of software and hardware systems. We specify a mutual exclusion protocol and prove that it satisfies the desired requirements with the help of the tools provided by our general framework. Even though we use CafeOBJ for mechanical assistance for proofs, our goal is not to present CafeOBJ in detail, but rather its underlying logics. We develop an abstract proof calculus for logics whose sentences are universal Horn sentences of the form (∀X )(∧H ⇒ C) and prove an institution generalization of Birkhoff completeness theorem. This result is applied to Horn clause logic, the “Horn fragment” of preorder algebra, order-sorted algebra and partial algebra and their infinitary variants. The completeness of the infinitary logic L ω1 ,ω was proved by Carol Karp in 1964. We express and prove the completeness of infinitary first-order logics in the institution-independent setting by using forcing, a powerful method for constructing models. As a consequence of this abstraction, our results become available for the infinitary versions of many first-order logical systems. Although we emphasize the results for the infinitary logics our framework covers also the finitary cases. Many computer science applications concern properties which are true of a restricted class of models, in most of the cases reachable models with constructor-generated elements. We introduce the concept of reachable model in the institution model theory. We present a couple of constructor-based institutions defined on top of the Horn and first-order institutions, basically by restricting the class of models to the reachable models. We define the proof rules for these logics, and lift the completeness results previously obtained to the constructor-based logics using institution-independent techniques.. i.
(4)
関連したドキュメント
Thus, in Section 5, we show in Theorem 5.1 that, in case of even dimension d > 2 of a quadric the bundle of endomorphisms of each indecomposable component of the Swan bundle
This is a consequence of a more general result on interacting particle systems that shows that a stationary measure is ergodic if and only if the sigma algebra of sets invariant
In [6], Chen and Saloff-Coste compare the total variation cutoffs between the continuous time chains and lazy discrete time chains, while the next proposition also provides a
A lemma of considerable generality is proved from which one can obtain inequali- ties of Popoviciu’s type involving norms in a Banach space and Gram determinants.. Key words
For example, a maximal embedded collection of tori in an irreducible manifold is complete as each of the component manifolds is indecomposable (any additional surface would have to
In [9], it was shown that under diffusive scaling, the random set of coalescing random walk paths with one walker starting from every point on the space-time lattice Z × Z converges
In this paper, we derive generalized forms of the Ky Fan minimax inequality, the von Neumann-Sion minimax theorem, the von Neumann-Fan intersection theorem, the Fan-type
“Breuil-M´ezard conjecture and modularity lifting for potentially semistable deformations after
