Mechanizing Nonstandard Real Analysis (Q4504968)
From MaRDI portal
scientific article; zbMATH DE number 1509489
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Mechanizing Nonstandard Real Analysis |
scientific article; zbMATH DE number 1509489 |
Statements
Mechanizing Nonstandard Real Analysis (English)
0 references
25 September 2000
0 references
hyperreals
0 references
theorem-prover Isabelle
0 references
higher-order logic
0 references
infinitesimals
0 references
infinite numbers
0 references
nonstandard analysis
0 references
filters
0 references
ultrafilters
0 references
mechanical theorem-proving
0 references
0 references
