6 citations · 10 across the 7 of their papers we have counts for
8 papers
Dedukti: a Logical Framework based on the -Calculus Modulo Theory
Ali Assaf, Guillaume Burel, Raphaël Cauderlier +7
Dedukti is a Logical Framework based on the -Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simpl…
A Simple Proof That Super-Consistency Implies Cut Elimination
Gilles Dowek, Olivier Hermant
We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simplification of the proof that supe…
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Frédéric Blanqui, Guillaume Genestier, Olivier Hermant
Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this tech…
Runtime Analysis of Whole-System Provenance
Thomas Pasquier, Xueyuan Han, Thomas Moyer +5
Identifying the root cause and impact of a system intrusion remains a foundational challenge in computer security. Digital provenance provides a detailed history of the flow of inf…
Polarized Rewriting and Tableaux in B Set Theory
Olivier Hermant
We propose and extension of the tableau-based first-order automated theorem prover Zenon Modulo to polarized rewriting. We introduce the framework and explain the potential benefit…
A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization
Richard Bonichon, Olivier Hermant
We prove the syntactic soundness of classical tableaux with free variables and on-the-fly Skolemization. Soundness proofs are usually built from semantic arguments, and this is to…
Semantic A-translation and Super-consistency entail Classical Cut Elimination
Lisa Allali, Olivier Hermant
We show that if a theory R defined by a rewrite system is super-consistent, the classical sequent calculus modulo R enjoys the cut elimination property, which was an open question.…
Polarizing Double Negation Translations
Mélanie Boudard, Olivier Hermant
Double-negation translations are used to encode and decode classical proofs in intuitionistic logic. We show that, in the cut-free fragment, we can simplify the translations and in…