An Automation-Friendly Set Theory for the B Method

DOI10.1007/978-3-319-91271-4_32MaRDI QIDQ5881455zbMATH OpenOpenAlexFDO

Authors Guillaume Bury, Simon Cruanes, David Delahaye

Publication date 10 March 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-91271-4_32

zbMATH Keywords

automated deductionB-methodpolymorphic typesrewritingset theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Set theory (03E99) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• The B-Book
• Theorem proving modulo

Cited in

(4)

• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Soundly proving B method formulæ using typed sequent calculus
• scientific article; zbMATH DE number 1765668 (Why is no real title available?)

Describes a project that uses

Uses Software

• BWare
• Easychair

This page was built for publication: An Automation-Friendly Set Theory for the B Method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5881455)