相关论文: Set-theoretical mathematics in Coq

In domain theory every finite computable object can be represented by a single mathematical object instead of a set of objects, using the notion of finitary-basis. In this article we report on our effort to formalize domain theory in Coq in…

In France, the first year of study at university is usually abbreviated L1 (for premiere annee de Licence). At Sorbonne Paris Nord University, we have been teaching an 18 hour introductory course in formal proofs to L1 students for 3 years.…

The purpose of this paper is to extend the cohomology and conformal derivation theories of the classical Lie conformal algebras to Hom-Lie conformal algebras. In this paper, we develop cohomology theory of Hom-Lie conformal algebras and…

In this paper, we determine the complexity of the satisfiability problem for various logics obtained by adding numerical quantifiers, and other constructions, to the traditional syllogistic. In addition, we demonstrate the incompleteness of…

We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. ${\rm CTT}_{\rm qe}$ is a version of Church's type…

In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and…

We give formal content to some concepts, naturally stemming from consistent history approach (CHA), which are not formalized in the standard formulation of the theory. The outcoming (extended) conceptual basis is used to perform a formal,…

We use automated theorem provers to significantly shorten a formal development in higher order set theory. The development includes many standard theorems such as the fundamental theorem of arithmetic and irrationality of square root of…

In this paper we address the decision problem for a fragment of set theory with restricted quantification which extends the language studied in [4] with pair related quantifiers and constructs, in view of possible applications in the field…

The importance of category theory in recent developments in both mathematics and in computer science cannot be overstated. However, its abstract nature makes it difficult to understand at first. Graphical languages have been developed to…

Fractional calculus is a generalization of classical theories of integration and differentiation to arbitrary order (i.e., real or complex numbers). In the last two decades, this new mathematical modeling approach has been widely used to…

We give an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This is based on my talk at the PQR conference (Brussels, June 2003).

I survey problems concerning Lindelof spaces which have partial set- theoretic solutions.

Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for…

Interpretational problems with quantum mechanics can be phrased precisely by only talking about empirically accessible information. This prompts a mathematical reformulation of quantum mechanics in terms of classical mechanics. We survey…

The theorem of three circles in real algebraic geometry guarantees the termination and correctness of an algorithm of isolating real roots of a univariate polynomial. The main idea of its proof is to consider polynomials whose roots belong…

Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof…

Two methods for extracting detailed formal dependencies from the Coq and Mizar system are presented and compared. The methods are used for dependency extraction from two large mathematical repositories: the Coq Repository at Nijmegen and…

Hammers are tools that provide general purpose automation for formal proof assistants. Despite the gaining popularity of the more advanced versions of type theory, there are no hammers for such systems. We present an extension of the…

The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We…