Banishing Ultrafilters from Our Consciousness

DOI10.1007/978-3-319-41842-1_10zbMath1439.03034OpenAlexW2584130636MaRDI QIDQ3305324

Alberto Policriti, Domenico Cantone, Eugenio Giovanni Omodeo

Publication date: 6 August 2020

Published in: Outstanding Contributions to Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-41842-1_10

zbMATH Keywords

nonstandard analysisproof checkingproof engineeringfoundations of infinitesimal calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Nonstandard models in mathematics (03H05) Other applications of nonstandard models (economics, physics, etc.) (03H10)

Uses Software

• ACL2
• Isabelle/HOL

Cites Work

• Metamathematical extensibility for theorem verifiers and proof-checkers
• Non-resolution theorem proving
• The linked conjunct method for automatic deduction and related search techniques
• From Linear Operators to Computational Biology
• Formalization of real analysis: a survey of proof assistants and libraries
• Decision procedures for elementary sublanguages of set theory IX. Unsolvability of the decision problem for a restricted subclass of the Δ0-formulas in set theory
• A Free Variable Version of the First-Order Predicate Calculus
• Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
• Computational Logic and Set Theory
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Nonstandard analysis in ACL2
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Banishing Ultrafilters from Our Consciousness