Authors
Claus-Peter Wirth
Title
Descente Infinie + Deduction
In
Logic Journal of the IGPL, Vol. 12(1), pp. 1-96, January 2004
Bibtex Entry
Copyright
Oxford University Press
Up-to-dateness
Optimal. Accepted version, submitted September 12, 2003. Only superficial corrigenda.
There is also an older version.
Abstract
Inductive theorem proving in the form of descente infinie was known to the ancient Greeks and is the standard induction method of a working mathematician since it was reinvented in the middle of the 17th century. We present an integration of descente infinie into state-of-the-art free-variable sequent and tableau calculi. It is well-suited for an efficient interplay of human interaction and automation and combines raising, explicit representation of dependence between variables, the liberalized delta-rule, preservation of solutions, and unrestricted applicability of lemmas and induction hypotheses. The semantical requirements are satisfied for a variety of two-valued logics, such as clausal logic, classical first-order logic, and higher-order modal logic.
Full paper
Official version with journal cover. Beware: Prints out page 1 on page 6 ("uneven to even" error)!
  • Format
    pdf
    Size
    0.9 Mbytes
Official version with journal cover, but nicely printing page 1 as uneven.
  • Format
    .ps.gz
    Size
    0.7 Mbytes
Versions without journal cover and proper volume number, but with corrigenda incorporated
  • File in dvi
    all.dvi
    Size
    0.2 Mbytes
  • File in ps.gz
    all.ps.gz
    Size
    0.4 Mbytes
  • File in searchable pdf
    pdf.pdf
    Size
    0.7 Mbytes
Application for a DFG research grant; submitted June 30, 2004. Rejected January 4, 2005; the reviews show no sign of any knowledge on deduction, but of ignorance on induction only. I would like to publish the whole evalution data as an example for the DFG's inability to evaluate non-trivial proposals.
Carefully typeset original
  • Format
    pdf
    Size
    0.5 Mbytes
    Format
    ps.gz
    Size
    0.4 Mbytes
    Format
    dvi
    Size
    0.1 Mbytes
The fonts of this version differ from the original, some originally identical fonts are different in this version, but the whole file can be searched!
  • File
    pdf
    Size
    0.3 Mbytes
Related Talk
Ceterum censeo Descente Infinie esse disputandam