Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Experience with FS0 as a framework theory

Matthews, Seán and Smaill, Alan and Basin, David A.

MPI-I-92-214. March 1992, 25 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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
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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-92-214.pdfMPI-I-92-214.pdfMPI-I-92-214.dvi107 KBytes; 10318 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Matthews, Se{\'a}n and Smaill, Alan and Basin, David A.},
  TITLE = {Experience with FS0 as a framework theory},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-92-214},
  MONTH = {March},
  YEAR = {1992},
  ISSN = {0946-011X},