About: A Formalization of Properties of Continuous Functions on Closed Intervals

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: A Formalization of Properties of Continuous Functions on Closed Intervals Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : covidontheweb.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	A Formalization of Properties of Continuous Functions on Closed Intervals
Creator	Yu, Wensheng Fu, Yaoshun
Source	PMC
abstract	Formal mathematics is getting increasing attention in mathematics and computer science. In particular, the formalization of calculus has important applications in engineering design and analysis. In this paper, we present a formal proof of some fundamental theorems of continuous functions on closed intervals based on the Coq proof assistant. In this formalization, we build a real number system referring to Landau’s Foundations of Analysis. Then we complete the formalization of the basic definitions of interval, function, and limit and formally prove the theorems including completeness theorem, intermediate value theorem, uniform continuity theorem and others in Coq. The proof process is normalized, rigorous and reliable.
has issue date	2020-06-06(xsd:dateTime)
bibo:doi	10.1007/978-3-030-52200-1_27
has license	no-cc
sha1sum (hex)	a4d63f60e041a17162bf22ea443690db51830716
schema:url	https://doi.org/10.1007/978-3-030-52200-1_27
resource representing a document's title	A Formalization of Properties of Continuous Functions on Closed Intervals
has PubMed Central identifier	PMC7340941
schema:publication	Mathematical Software - ICMS 2020
resource representing a document's body	covid:a4d63f60e041a17162bf22ea443690db51830716#body_text
is schema:about of	named entity 'interval' named entity 'applications' named entity 'computer science' named entity 'completeness theorem' named entity 'Functions' named entity 'PRESENT' named entity 'Coq' named entity 'referring' named entity 'uniform continuity' named entity 'fundamental theorems' named entity 'formalization' named entity 'mathematics' named entity 'intermediate value theorem' named entity 'Continuous Functions' named entity 'Closed Intervals' named entity 'real numbers' named entity 'uniform continuity' named entity 'upper bound' named entity 'Coq' named entity 'Peano' named entity 'non-empty' named entity 'Corollary' named entity 'Upper bound' named entity 'Extreme value theorem' named entity 'Uniform continuity' named entity 'real number' named entity 'multiplication' named entity 'Weierstrass' named entity 'Boundedness theorem' named entity 'law of excluded middle' named entity 'closed intervals' named entity 'continuous functions' named entity 'Dedekind' named entity 'left continuous' named entity 'Supremum' named entity 'number theory' named entity 'Uniform continuity' named entity 'Cauchy' named entity 'Coq' named entity 'real numbers' named entity 'formal proofs' named entity 'naive set theory' named entity 'calculus' named entity 'number theory' named entity 'real number' named entity 'continuous functions' named entity 'rational number' named entity 'Intermediate value theorem' named entity 'formal definition' named entity 'number theory' named entity 'space and time' named entity 'supremum' named entity 'signal processing' named entity 'Germany' named entity 'closed intervals' named entity 'lower bound' named entity 'Cauchy' named entity 'Gödel's first incompleteness theorem' named entity 'research teams' named entity 'Continuous functions' named entity 'Bolzano' named entity 'Coq' named entity 'upper bound' named entity 'Bolzano' named entity 'set theory' named entity 'github.com' named entity 'Lemma' named entity 'Coq' named entity 'HOL Light' named entity 'recursively define' named entity 'Coq' named entity 'Weierstrass' named entity 'number theory' named entity 'Bolzano' named entity 'continuous functions' named entity 'supremum' named entity 'history of mathematics' named entity 'Uniform continuity' named entity 'mathematics' named entity 'differential calculus' named entity 'positive integers' named entity 'supremum'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software