Skip to main content
SpringerLink
Log in

Full First-Order Free Variable Sequents and Tableaux in Implicit Induction

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1999)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1617))

Abstract

We show how to integrate implicit inductive theorem proving into free variable sequent and tableau calculi and compare the appropriateness of tableau calculi for this integration with that of sequent calculi.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Matthias Baaz, Uwe Egly, Christian G. Fermüller (1997). Lean Induction Principles for Tableaux. 6thTABLEAUX1997, LNAI1227, pp. 62–75, Springer.

    Google Scholar 

  • Leo Bachmair (1988). Proof By Consistency in Equational Theories. 3rd IEEE symposium on Logic In Computer Sci., pp. 228–233, IEEE Press.

    Google Scholar 

  • Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg (1997). Computing Answers with Model Elimination. Artificial Intelligence 90, pp. 135–176.

    Article  MATH  MathSciNet  Google Scholar 

  • Herbert B. Enderton (1973). A Mathematical Introduction to Logic. Academic Press.

    Google Scholar 

  • Melvin Fitting (1996). First-Order Logic and Automated Theorem Proving. 2nd extd. ed., Springer.

    Google Scholar 

  • Gerhard Gentzen (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, pp. 176–210, 405–431.

    Article  MathSciNet  Google Scholar 

  • Alfons Geser (1995). A Principle of Non-Wellfounded Induction. In: Tiziana Margaria (ed.): Kolloquium Programmiersprachen und Grundlagen der Programmierung, MIP-9519, pp. 117–124, Univ. Passau.

    Google Scholar 

  • Ulrich Kühler (1999). A Tactic-Based Inductive Theorem Prover for Data Types with Partial Operations. Dissertation (Ph.D. thesis), Univ. Kaiserslautern, to appear.

    Google Scholar 

  • Ulrich Kühler, Claus-Peter Wirth (1996). Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. SEKI-Report SR-96-11, FB Informatik, Univ. Kaiserslautern. Short version in: 8th RTA 1997, LNCS 1232, pp. 38–52, Springer.

    Google Scholar 

  • Peter Padawitz (1996). Inductive Theorem Proving for Design Specifications. J. Symbolic Computation 21, pp. 41–99, Academic Press.

    Article  MATH  MathSciNet  Google Scholar 

  • Dag Prawitz (1960). An Improved Proof Procedure. In: Siekmann & Wrightson (1983), Vol. 1, pp. 159–199.

    Google Scholar 

  • Herman Rubin, Jean E. Rubin (1985). Equivalents of the Axiom of Choice. Elsevier.

    Google Scholar 

  • Jörg Siekmann, G. Wrightson (eds.) (1983). Automation of Reasoning. Springer.

    Google Scholar 

  • Raymond M. Smullyan (1968). First-Order Logic. Springer.

    Google Scholar 

  • Claus-Peter Wirth (1997). Positive/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving. Dissertation (Ph.D. thesis), Verlag Dr. Kovač, Hamburg.

    Google Scholar 

  • Claus-Peter Wirth (1998). Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but Without Skolemization. Report 698/1998, FB Informatik, Univ. Dortmund. Short version in: Gernot Salzer, Ricardo Caferra (eds.). Proc. 2nd Int. Workshop on First-Order Theorem Proving (FTP), pp. 244–255, Vienna, 1998. Also submitted for LNCS version, Springer, 1999.

    Google Scholar 

  • Claus-Peter Wirth, Klaus Becker (1995). Abstract Notions and Inference Systems for Proofs by Mathematical Induction. 4thCTRS1994, LNCS968, pp. 353–373, Springer.

    Google Scholar 

  • Claus-Peter Wirth, Bernhard Gramlich (1994). On Notions of Inductive Validity for First-Order Equational Clauses. 12thCADE1994, LNAI814, pp. 162–176, Springer.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität Dortmund, Informatik 5, D-44221, Germany

    Claus-Peter Wirth

Authors
  1. Claus-Peter Wirth
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Institute for Programming and Logics, University at Albany - SUNY, Albany, NY, 12222, USA

    Neil V. Murray

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Heidelberg Berlin

About this paper

Cite this paper

Wirth, CP. (1999). Full First-Order Free Variable Sequents and Tableaux in Implicit Induction. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_25

Download citation

  • DOI: https://doi.org/10.1007/3-540-48754-9_25

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66086-6

  • Online ISBN: 978-3-540-48754-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation