Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

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
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger
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 24 septembre 2020 - 16:36:04
Archivage à long terme le : : mardi 25 septembre 2018 - 20:55:43

Fichiers

Vignette du document
main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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

Collections

ENSMP_CRI | PARISTECH | INSTITUT-TELECOM | ENSMP | 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⟩

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

113

Téléchargements de fichiers

36