Methods of Functional Extension

  • Matthias Baaz
  • Alexander Leitsch
Part of the Collegium Logicum book series (COLLLOGICUM, volume 1)


Functional extension is a principle which encodes the expressive power of quantifiers; it can be used to compute normal forms of formulas and as inference rule. The rôle of extension in computational calculi is analogous to that of cut in standard logic calculi; we provide evidence to this statement by presenting several results on proof complexity and extension (particularly effects of nonelementary speed-up of proof length). Moreover, we compare calculi of function introduction (based on Skolemization) whith Hilbert’s ε-calculus. Finally we use Hilbert’s ε-induction axioms to formulate a computational principle of Noetherian induction based on (Skolem) function introduction rules.


Predicate Logic Conjunctive Normal Form Predicate Symbol Automate Deduction Functional Extension 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Aubin 1979]
    R. Aubin: Mechanizing Structural Induction I, II. Theoretical Computer Science 9 (1979) 329–362.MathSciNetMATHCrossRefGoogle Scholar
  2. [Baaz, Fermüller 1992]
    M. Baaz, Ch. G. Fermüller: Resolution for many-valued logics. In: A. Voronkov (ed.), Logic Programming and Automated Reasoning. Proc. LPAR’92, LNAI 624, pp. 107–118, Springer, Berlin, 1992.CrossRefGoogle Scholar
  3. [Baaz, Fermüller, Leitsch 1994]
    M. Baaz, Ch. G. Fermüller, A. Leitsch: A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation. Proc. 9th LICS Symposium, IEEE Computer Society Press, Paris, 1994, pp. 213–219.Google Scholar
  4. [Baaz, Leitsch 1992]
    M. Baaz, A. Leitsch: The Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic 5 (1992) 181–215.MathSciNetCrossRefGoogle Scholar
  5. [Baaz, Leitsch 1994]
    M. Baaz, A. Leitsch: On Skolemization and proof complexity. Fundamenta Informaticae 20 /4 (1994).Google Scholar
  6. Darlington 1968] J. L. Darlington: Automatic theorem proving with equality substitutions and mathematical induction. Machine Intelligence 3, American Elsevier, New York, pp. 113–127.Google Scholar
  7. [Eder 1992]
    E. Eder: Relative Complexities of First Order Calculi. Vieweg, Wiesbaden, 1992.Google Scholar
  8. [Egly 1990]
    U. Egly: Problem-Reduction Methods and Clause Splitting in Automated Theorem Proving. Master Thesis ( Computer Science ), Univ. of Technology Vienna, 1990.Google Scholar
  9. [Egly 1991]
    U. Egly: A generalized factorization rule based on the introduction of Skolem terms. In: H. Kaindl (ed.), Österr. Artificial Intelligence Tagung, Springer, Berlin, Heidelberg, New York (1991), pp. 116–125.Google Scholar
  10. [Egly 1992]
    U. Egly: Shortening Proofs by Quantifier Introduction. Proc. of the LPAR’92, LNAI 624, pp. 148–159, Springer, Berlin, 1992.Google Scholar
  11. [Egly 1994]
    U. Egly: Function Introduction and the Complexity of Proofs. Ph. Thesis ( Computer Science ), Univ. of Darmstadt, 1994.Google Scholar
  12. [Haken 1985]
    A. Haken: The intractability of resolution. Theoret. Comput. Sci. 39 (2&3) (1985) 297–308.MathSciNetMATHCrossRefGoogle Scholar
  13. [Hilbert, Bernays 1970]
    D. Hilbert, P. Bernays: Grundlagen der Mathematik II, 2. Auflage. Springer, Berlin, Heidelberg, New York, 1970.Google Scholar
  14. [Krajiček, Pudlák 1988]
    J. Krajiček, P. Pudlák: The number of proof lines and the size of proofs in first order logic. Arch. Math. Logic 27 (1988) 69–84.MathSciNetMATHCrossRefGoogle Scholar
  15. [Orevkov 1979]
    V. P. Orevkov: Lower Bounds for Increasing Complexity of Derivations after Cut Elimination (translation). In: Journal of Soviet Mathematics, 2337–2350, 1982.Google Scholar
  16. [Mints 1990]
    G. Mints: Gentzen-type systems and resolution rules. Part I: Propositional logic. In: Proc. COLOG’88, LNCS 417, pp. 198–231, Springer, Berlin, 1990.Google Scholar
  17. [Mints 1993]
    G. Mints: Gentzen-type systems and resolution rules. Part II: Predicate logic. In: Proc. Logic Colloquium 1990, Lecture Notes in Logic, vol. 2, Springer, Berlin, 1993.Google Scholar
  18. [Musser 1980]
    D. R. Musser: On Proving Inductive Properties of Abstract Data Types. Proc. 7 Symp. on Principles of Programming Languages, Las Vegas (1980) 154–162.Google Scholar
  19. [Pelletier 1986]
    F. J. Pelletier: Seventy-five problems for testing automatic theorem provers. J. of Automated Reasoning 2 (1986) 181–216.MathSciNetCrossRefGoogle Scholar
  20. [Reddy 1990]
    U. S. Reddy: Term Rewriting Induction. 10 CADE 1990, LNAI 449, pp. 162–177, Springer, Berlin, 1990.Google Scholar
  21. [Shoenfield 1967]
    J. R. Shoenfield: Mathematical Logic. Addison-Wesley, 1967.Google Scholar
  22. [Statman 1974]
    R. Statman: Structural Complexity of Proof. Dissertation, Stanford University, 1974.Google Scholar
  23. [Statman 1979]
    R. Statman: Lower bounds on Herbrand’s theorem. Proc. Amer. Math. Soc. 75 (1979) 104–107.MathSciNetMATHGoogle Scholar
  24. [Takeuti 1987]
    G. Takeuti: Proof Theory; 2nd edition. Studies in Logic 81, North-Holland, Amsterdam, 1987.Google Scholar
  25. [Tseitin 1970]
    G. S. Tseitin: On the Complexity of Derivation in Propositional calculus. In: Automation of Reasoning 2, Eds. J. Siekmann, G. Wrightson, Springer, New York, 1983.Google Scholar
  26. [Yukami 1984]
    T. Yukami: Some results on speed-up. Ann. Japan Assoc. Philos. Sci. 6 (1984) 195–205.MathSciNetMATHGoogle Scholar

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • Matthias Baaz
    • 1
  • Alexander Leitsch
    • 2
  1. 1.Institut für Algebra und Diskrete MathematikTechnische Universität WienWienAustria
  2. 2.Institut für ComputersprachenTechnische Universität WienWienAustria

Personalised recommendations