Skip to Main content Skip to Navigation
Conference papers

Polarized Rewriting and Tableaux in B Set Theory

Olivier Hermant 1, 2
1 MINES ParisTech - École nationale supérieure des mines de Paris
2 CRI - Centre de Recherche en Informatique
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.
Mots-clés : théorie des ensembles démonstration automatique tableaux déduction modulo théorie méthode B
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
https://hal-mines-paristech.archives-ouvertes.fr/hal-01820522
Contributor : Claire Medrala <>
Submitted on : Thursday, June 21, 2018 - 5:49:13 PM
Last modification on : Thursday, September 24, 2020 - 4:36:04 PM
Long-term archiving on: : Tuesday, September 25, 2018 - 8:55:43 PM

Files

Vignette du document
main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01820522, version 1
  • ARXIV : 1806.08536

Collections

INSTITUT-TELECOM | ENSMP | ENSMP_CRI | PARISTECH | PSL

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

129

Files downloads

49