Automatically assigned DDC number:

Manually assigned DDC number: 005131

Title: Linking Notations and Theories in a Proof Tool

Author:

Subject: Rachel Cardell-oliver Linking Notations and Theories in a Proof Tool

Description: . The formal development of non-trivial, real-time systems can be made more manageable by using several complementary formal methods for different aspects of the development. In this paper we show how sound interfaces between different methods can be defined formally in the HOL theorem proving system and how we have used such links to solve a variety of problems. Our motivation for linking theories is pragmatic. In a number of case studies different theories have been linked in order to make specification and verification more manageable and even to make it feasible. This paper offers a formal framework for defining and implementing links between theories. Because both object language and meta language are visible in the HOL system, and the system itself can communicate with other systems, it is possible to define explicitly and formally links of different "weight". 1 Introduction The formal development of non-trivial, real-time systems can be made more manageable by using several com...

Contributor: The Pennsylvania State University CiteSeer Archives

Publisher: unknown

Date: 1998-03-12

Pubyear: unknown

Format: ps

Identifier: http://citeseer.ist.psu.edu/140196.html

Source: http://kidwelly.cam.sri.com/tr/crc058/paper.ps.Z

Language: en

Rights: unrestricted