Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto

DOI10.1093/JIGPAL/JZR048zbMath1314.03019OpenAlexW3100894027MaRDI QIDQ4913999

Claus-Peter Wirth

Publication date: 17 April 2013

Published in: Logic Journal of IGPL (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/jigpal/jzr048

zbMATH Keywords

automated theorem provingmathematical inductionripplingproof planninghuman-oriented theorem provingrecursion analysisFermat's descente infinie

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (1)

Herbrand's fundamental theorem in the eyes of Jean van Heijenoort

Uses Software

• NQTHM
• Waldmeister
• Lambda-Clam
• CLAM
• Oyster
• QuodLibet
• Unnamed Item
• Unnamed Item

This page was built for publication: Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto