# Item

ITEM ACTIONSEXPORT

Released

Report

#### Experience with FS0 as a framework theory

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

MPI-I-92-214.pdf

(Any fulltext), 11MB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

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

##### Abstract

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.