Polarized Rewriting and Tableaux in B Set Theory

Olivier Hermant (1, 2)

1 Mines Paris - PSL (École nationale supérieure des mines de Paris)
2 CRI - Centre de Recherche en Informatique

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.

Mots clés: démonstration automatique; théorie des ensembles; méthode B; déduction modulo théorie; tableaux

Domaines: Théorie et langage formel [cs.FL]

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⟩