Abstract : 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 benefits. The first target is an industrial benchmark composed of B Set Theory problems.
https://hal-mines-paristech.archives-ouvertes.fr/hal-01820522
Contributeur : Claire Medrala
<>
Soumis le : jeudi 21 juin 2018 - 17:49:13
Dernière modification le : jeudi 7 février 2019 - 14:49:15
Document(s) archivé(s) le : mardi 25 septembre 2018 - 20:55:43
Olivier Hermant. Polarized Rewriting and Tableaux in B Set Theory. 3RD INTERNATIONAL WORKSHOP ABOUT SETS AND TOOLS (SETS 2018), Jun 2018, Southampton, United Kingdom. pp.67-72. ⟨hal-01820522⟩
