Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques

DOI10.1145/322017.322018zbMATH Open0359.68109OpenAlexW2080104522MaRDI QIDQ4131708FDOQ4131708

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 analysis (26E35) Nonstandard models (03H99)

Cited In (7)

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

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)