Help Privacy Policy Disclaimer
  Advanced SearchBrowse





Experience with FS0 as a framework theory


Matthews,  Seán
Programming Logics, MPI for Informatics, Max Planck Society;

Smaill,  Alan
Programming Logics, MPI for Informatics, Max Planck Society;


Basin,  David
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Any fulltext), 11MB

Supplementary Material (public)
There is no public supplementary material available

Matthews, S., Smaill, A., & Basin, D.(1992). Experience with FS0 as a framework theory (MPI-I-92-214). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B727-3
The report is a draft version of the first six chapters of a book which is attempting to supply a comprehensive coverage of the mathematical and computational aspects of temporal logic. The first chapter introduces temporal logic and gives a fairly detatiled preview of the issues which will be covered in the rest of the whole book. These include expressive power, fixed point temporal languages and applications in computing. Chapter 2 develops the basic idea of a language built from connectives whose semantics is appropriate to some class of underlying ``models" of time: for example linear or branching time. Chapter 3 introduces Hilbert style axiomatizations of such logics and contains some simple completeness proofs. The incomplete chapter 4 considers the generally incomplete predicate temporal languages and gives examples of some of the variety of choices of language here. In Chapter 5 we debate the merits of using classical first order logic to talk about temporal structures from the ``outside" instead of using temporal languages ``inside" the structure. We also consider the possibility of using temporal logic itself as a metalanguage. Finally, in chapter 6 we present a general theory of axiomatization of temporal logics. This examines and uses the irreflexivity rule of Gabbay to provide very general techniques. Feferman has proposed a system, as an alternative framework for encoding logics and also for reasoning about those encodings. We have implemented a version of this framework and performed experiments that show that it is practical. Specifically, we describe a formalisation of predicate calculus and the development of an admissible rule that manipulates formulae with bound variables. This application will be of interest to researchers working with frameworks that use mechanisms based on substitution in the lambda calculus to implement variable binding and substitution in the declared logic directly. We suggest that meta-theoretic reasoning, even for a theory using bound variables, is not as difficult as is often supposed, and leads to more powerful ways of reasoning about the encoded theory.