45 citations · 56 across the 9 of their papers we have counts for
10 papers
Geometric theories for real number algebra without sign test or dependent choice axiom
Henri Lombardi, 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…
Machine-Checked Categorical Diagrammatic Reasoning
Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez
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 librar…
A First Order Theory of Diagram Chasing
Assia Mahboubi, Matthieu Piquerez
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 chas…
Trocq: Proof Transfer for Free, With or Without Univalence
Cyril Cohen, Enzo Crance, Assia Mahboubi
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…
Valuative lattices and spectra
Henri Lombardi, Assia Mahboubi
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 m…
Compositional pre-processing for automated reasoning in dependent type theory
Valentin Blot, Denis Cousineau, Enzo Crance +4
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…
A Formal Proof of the Irrationality of
Assia Mahboubi, Thomas Sibut-Pinote
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 fi…
Axiomatic constraint systems for proof search modulo theories
Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand +2
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…
Two simulations about DPLL(T)
Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
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 formulatio…
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
Assia Mahboubi, Cyril Cohen
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,…