MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


On natural deduction in fixpoint logics

Szalas, Andrzej

February 1992, 18 pages.

Status: available - back from printing

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.

  • MPI-I-92-203.pdfMPI-I-92-203.pdfMPI-I-92-203.dvi
  • Attachement: MPI-I-92-203.dvi (71 KBytes); MPI-I-92-203.pdf (121 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  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},