Showing cs.LOShow all
3 papers · 1 filter
cs.LO2019
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…
cs.LO2018
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…
cs.LO2015
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…