Thursday 11 July 2019, 14:00, LSV library: Orienting Axioms into Rewriting Rules - Proof of Concept, Guillaume Rousseau (L3 intern, ENS Lyon).

In deduction modulo, a first-order theory may be presented as a set of rewriting rules. Natural deduction, resolution, tableaux methods and other concepts are expanded with these rewriting rules, which may hasten proof search for formulas. I will present the performances of three solvers (ArchSAT, Zipperposition and iProverModulo) which were given a wide array of problems, whose axioms were transformed into different rewriting systems, and show that the results are very promising.