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

MPI-I-92-203

On natural deduction in fixpoint logics

Szalas, Andrzej

MPI-I-92-203. February 1992, 18 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
In the current paper we present a powerful technique of obtaining natural deduction (or, in other words, Gentzen-like) proof systems for first-order fixpoint logics. The term "fixpoint logics" refers collectively to a class
of logics consisting of modal logics with modalities definable at meta-level by fixpoint equations on formulas.
The class was found very interesting as it contains most logics of programs with e.g. dynamic logic, temporal logic and, of course, mu-calculus among them.

Fixpoint logics were intensively studied during the last decade. In this paper we are going to present some results concerning deductive systems for first-order fixpoint logics. In particular we shall present some powerful and general technique for obtaining natural deduction (Gentzen-like) systems for fixpoint logics. As those logics are usually totally undecidable, we show how to obtain complete (but infinitary) proof systems as well as relatively complete (finitistic) ones. More precisely, given fixpoint equations on formulas defining nonclassical connectives of a logic, we automatically derive Gentzen-like proof systems for the logic. The discussion of implementation problems is also provided.
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-203.pdfMPI-I-92-203.pdfMPI-I-92-203.dvi71 KBytes; 121 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: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-203
Hide details for BibTeXBibTeX
@TECHREPORT{Szalas92a,
  AUTHOR = {Szalas, Andrzej},
  TITLE = {On natural deduction in fixpoint logics},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-92-203},
  MONTH = {February},
  YEAR = {1992},
  ISSN = {0946-011X},
}