max planck institut

informatik

informatik

**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

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.

Acknowledgement:** **

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.pdf | 107 KBytes; 10318 KBytes |

Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView |