An Automation-Friendly Set Theory for the B Method

Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard
Digital Printed Abstract View Cite
Type
Short Paper
Publication
6th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'18)

Abstract

We propose an automation-friendly set theory for the B method. This theory is expressed using first order logic extended to polymorphic types and rewriting. Rewriting is introduced along the lines of deduction modulo theory, where axioms are turned into rewrite rules over both propositions and terms. We also provide experimental results of several tools able to deal with polymorphism and rewriting over a benchmark of problems in pure set theory (i.e. without arithmetic).

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{BuryCDE18,
  author       = {Guillaume Bury and
                  Simon Cruanes and
                  David Delahaye and
                  Pierre{-}Louis Euvrard},
  editor       = {Michael J. Butler and
                  Alexander Raschke and
                  Thai Son Hoang and
                  Klaus Reichl},
  title        = {An Automation-Friendly Set Theory for the {B} Method},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
                  Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10817},
  pages        = {409--414},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-91271-4\_32},
  doi          = {10.1007/978-3-319-91271-4\_32},
  timestamp    = {Sun, 06 Oct 2024 20:56:29 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BuryCDE18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'18

Related