Encoding TLA+ set theory into many-sorted first-order logic

Abstract : We present an encoding of Zermelo-Fraenkel set theory into many-sorted first-order logic, the input language of state-of-the-art SMT solvers. This translation is the main component of a back-end prover based on SMT solvers in the TLA+ Proof System.
Type de document :
Pré-publication, Document de travail
2015
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01244627
Contributeur : Stephan Merz <>
Soumis le : mercredi 16 décembre 2015 - 09:13:21
Dernière modification le : mercredi 8 novembre 2017 - 12:08:09
Document(s) archivé(s) le : jeudi 17 mars 2016 - 11:30:18

Fichier

sets2015.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01244627, version 1
  • ARXIV : 1508.03838

Collections

Citation

Stephan Merz, Hernán Vanzetto. Encoding TLA+ set theory into many-sorted first-order logic. 2015. 〈hal-01244627〉

Partager

Métriques

Consultations de la notice

186

Téléchargements de fichiers

58