A predicate calculus with control of derivations

  • Daniel Mey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 440)


A fragment of classical predicate calculus which does not contain rules for contraction is defined. It is shown to be decidable and yet propositionally complete. A semantics which reflects its constructive character is developed.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BJ]
    G. Boolos and R. Jeffrey. Computability and logic. Cambridge university press (1974)Google Scholar
  2. [KP]
    J. Krajicek and P. Pudlak. The number of proof lines and the size of proofs in the first order logic. Archive for mathematical logic 27 (1988) 69–84Google Scholar
  3. [KW]
    J. Ketonen, R. Weyhrauch. A decidable fragment of predicate calculus. Theoretical computer science (TCS) 32 (1984) 297–307Google Scholar
  4. [Gi]
    J-Y. Girard. Linear logic. TCS 50 (1987) 1–101CrossRefGoogle Scholar
  5. [GL]
    J-Y. Girard, Y. Lafont. Linear logic and lazy computation. Proceedings theory and practice of software development 1987 (H. Ehrig et al., editors). Lecture notes in computer science 250 (1987) 52–66Google Scholar
  6. [AV]
    A. Avron. The semantics and proof theory of linear logic. TCS 57 (1988) 161–184Google Scholar
  7. [OK]
    H. Ono and Y. Komori. Predicate logic without the structure rules. Studia logica 45 (1985) 393–404.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Daniel Mey
    • 1
  1. 1.Institut für theoretische InformatikETH ZentrumZürich

Personalised recommendations