Assia Mahboubi
In this memoir, we seek to construct a constructive theory that is as complete as possible to describe the algebraic properties of the real number field in constructive mathematics without a dependent choice axiom. To this purpose, we use a…
In this memoir, we seek to construct a dynamical theory as complete as possible to describe the algebraic properties of the field of real numbers in constructive mathematics without axiom of dependent choice. We propose a theory which turns…
This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language,…
In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical…
Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of…
This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order…
The first part of the present article consists in a survey about the dynamical constructive method designed using dynamical theories and dynamical algebraic structures. Dynamical methods uncovers a hidden computational content for numerous…
This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant. This result was first presented by Ap\'ery in 1978, and the proof we have…
Goal-directed proof search in first-order logic uses meta-variables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific…
This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic…
In this paper we relate different formulations of the DPLL(T) procedure. The first formulation is based on a system of rewrite rules, which we denote DPLL(T). The second formulation is an inference system of, which we denote LKDPLL(T). The…