Mathematical induction in Otter-lambda

DOI10.1007/s10817-006-9036-zzbMath1107.68093OpenAlexW2033513250WikidataQ115056505 ScholiaQ115056505MaRDI QIDQ861715

Michael J. Beeson

Publication date: 30 January 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-006-9036-z

zbMATH Keywords

unificationmathematical inductionautomated deductioncomputer proofsfirst-order prover

Mathematics Subject Classification ID

Related Items

Mathematical induction in Otter-lambda ⋮ LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) ⋮ Automated reasoning with power maps ⋮ Translating higher-order clauses to first-order clauses ⋮ Unprovability results for clause set cycles ⋮ Commutativity Theorems in Groups with Power-like Maps

Uses Software

• TPS
• OTTER
• NQTHM
• MathXpert
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Mathematical induction in Otter-lambda
• Automated reasoning about elementary point-set topology
• Mechanizing structural induction. I: Formal system
• Mechanizing structural induction. II: Strategies
• TPS: A theorem-proving system for classical type theory
• Automated Reasoning
• A Fascinating Country in the World of Computing