4 papers
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…