A formalisation of consistent consequence for Boolean equation systems

DOI10.1007/978-3-319-66107-0_29MaRDI QIDQ1687766zbMATH OpenOpenAlexFDO

Authors Myrthe van Delft, Herman Geuvers, T. A. C. Willemse

Publication date 4 January 2018

Full work available at URL https://doi.org/10.1007/978-3-319-66107-0_29

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Consistent consequence for Boolean equation systems
• Proof by consistency in conditional equational theories
• Consistent correlations for parameterised Boolean equation systems with applications in correctness proofs for manipulations
• CONCUR 2004 - Concurrency Theory
• scientific article; zbMATH DE number 432735
• A Boolean computation approach of formal concepts
• Theory and Applications of Satisfiability Testing
• scientific article; zbMATH DE number 7204433
• Proof graphs for parameterised Boolean equation systems
• Publication:4487297

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• Abstraction in fixpoint logic
• An overview of the mCRL2 toolset and its recent advances
• Compositional verification of asynchronous concurrent systems using CADP
• Consistent consequence for Boolean equation systems
• Consistent correlations for parameterised Boolean equation systems with applications in correctness proofs for manipulations
• Introduction to bisimulation and coinduction
• Liveness analysis for parameterised Boolean equation systems

Cited in

(4)

• Instantiation for Parameterised Boolean Equation Systems
• Consistent consequence for Boolean equation systems
• Formal Systems for Tuple and Equality Generating Dependencies
• scientific article; zbMATH DE number 6130163 (Why is no real title available?)

Describes a project that uses

Uses Software

• mCRL2
• Coq

This page was built for publication: A formalisation of consistent consequence for Boolean equation systems

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