Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques

DOI10.1145/322017.322018MaRDI QIDQ4131708zbMATH OpenOpenAlexFDO

Authors A. M. Ballantyne, W. W. Bledsoe

Publication date 1977

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/322017.322018

Mathematics Subject Classification ID

Nonstandard models (03H99) Nonstandard analysis (26E35)

Cited in

(7)

• MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
• Knowledge-based proof planning
• A fully automatic theorem prover with human-style output
• Banishing ultrafilters from our consciousness
• Mechanizing Nonstandard Real Analysis
• An automatic proof of Gödel's incompleteness theorem
• Orderings for term-rewriting systems

This page was built for publication: Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques

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