Automatic derivation of the irrationality of \(e\)

DOI10.1006/jsco.2000.0465zbMath0981.68146OpenAlexW2078700544MaRDI QIDQ5950931

Michael J. Beeson

Publication date: 2 January 2002

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jsco.2000.0465

zbMATH Keywords

automatic generation of proofs

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items (6)

A fully automatic theorem prover with human-style output ⋮ Extending a Resolution Prover for Inequalities on Elementary Functions ⋮ MetiTarski: An automatic theorem prover for real-valued special functions ⋮ MetiTarski: An Automatic Prover for the Elementary Functions ⋮ Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

• OTTER
• HOL
• NQTHM
• Analytica
• Mathpert

Cites Work

• Thom's lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets
• USING NONSTANDARD ANALYSIS TO ENSURE THE CORRECTNESS OF SYMBOLIC COMPUTATIONS
• Some applications of Gentzen's proof theory in automated deduction
• Transcendental Numbers. (AM-16)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Automatic derivation of the irrationality of \(e\)