Automatic generation of epsilon-delta proofs of continuity

DOI10.1007/BFB0055903MaRDI QIDQ4217949zbMATH OpenFDO

Authors Michael Beeson

Publication date 11 November 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0055903

zbMATH Keywords

automatic generation of proofsepsilon-delta proofs of continuity

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Continuity and related questions (modulus of continuity, semicontinuity, discontinuities, etc.) for real functions in one variable (26A15)

Recommendations

• Automatic derivation of the irrationality of e
• scientific article; zbMATH DE number 1497745
• scientific article; zbMATH DE number 3938594
• A heuristic prover for elementary analysis in \textit{Theorema}
• Epsilon-delta proofs and uniform continuity

Cited in

(5)

• Constraint solving for proof planning
• Knowledge-based proof planning
• A fully automatic theorem prover with human-style output
• Now f is continuous (exercise!)
• Automatic derivation of the irrationality of e

Describes a project that uses

Uses Software

• Analytica

This page was built for publication: Automatic generation of epsilon-delta proofs of continuity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4217949)