- 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.
-
- 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!
-
- Related Talk
- Ceterum censeo Descente Infinie esse disputandam