-
Theorem Proving Modulo Revised Version
Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated... -
A Finite First-Order Presentation of Set Theory
We present a first-order formalization of set theory which has a finite number of axioms. Its syntax is similar to that often used in textbooks: it provides an... -
About Folding-Unfolding Cuts and Cuts Modulo
We show in this note that cut elimination in deduction modulo subsumes cut elimination in deduction with the folding and unfolding rules. -
Proof Normalization Modulo
Projet COQ -
Resolution is Cut-Free
International audience -
Narrowing Based Inductive Proof Search
Premiere version en 2005, en l'honneur de Harald Ganzinger -
Holls: an Intentional First-Order Expression of Higher-Order Logic
Projet COQ, Projet PARA, PROTHEO -
Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
International audience -
Semantic A-translation and Super-consistency entail Classical Cut Elimination
International audience -
Deduction and theorem proving modulo
Colloque sur invitation. -
Sequent Calculus Viewed Modulo
Colloque avec actes et comité de lecture. internationale. -
Theorem Proving Modulo
Article dans revue scientifique avec comité de lecture. internationale. -
Induction as Deduction Modulo
Rapport interne.
