Equivalence checking for orthocomplemented bisemilattices in log-linear time

DOI10.1007/978-3-030-99527-0_11MaRDI QIDQ6535616zbMATH OpenFDO

Authors Simon Guilloud, Viktor Kuncak

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-99527-0_11

Mathematics Subject Classification ID

Free lattices, projective lattices, word problems (06B25) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• On an equivalence checking technique for algebraic models of programs
• On the polynomial complexity of the equivalence checking problem in algebraic models of programs
• Formula normalizations in verification
• Fast algorithms for deciding the equivalence of propositional operator programs on ordered semigroup scales
• An implementation of an efficient algorithm for bisimulation equivalence

Cites work

• A Brief Overview of Mizar
• A machine program for theorem-proving
• A solution of the uniform word problem for ortholattices
• Automated complexity analysis based on ordered resolution
• Automatic recognition of tractability in inference relations
• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• Complete Sets of Reductions for Some Equational Theories
• Computer Aided Verification
• Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
• Decision procedures. An algorithmic point of view
• Free lattices.
• Free Ortholattices
• Hard examples for resolution
• HOL Light: An Overview
• scientific article; zbMATH DE number 3511563 (Why is no real title available?)
• scientific article; zbMATH DE number 1215500 (Why is no real title available?)
• scientific article; zbMATH DE number 1088188 (Why is no real title available?)
• scientific article; zbMATH DE number 3807678 (Why is no real title available?)
• On the Computational Complexity of Algebra on Lattices
• Proof Complexity
• Term Rewriting and All That
• The complexity of theorem-proving procedures
• The Isabelle Framework
• Topological sorting of large networks
• Untersuchungen über das logische Schliessen. I

Cited in

(1)

• Formula normalizations in verification

This page was built for publication: Equivalence checking for orthocomplemented bisemilattices in log-linear time

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