Equivalence checking for orthocomplemented bisemilattices in log-linear time
From MaRDI portal
Publication:6535616
DOI10.1007/978-3-030-99527-0_11zbMATH Open1547.68428MaRDI QIDQ6535616FDOQ6535616
Authors: Simon Guilloud, Viktor Kuncak 
Publication date: 1 February 2024
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
Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Free lattices, projective lattices, word problems (06B25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- The Isabelle Framework
- A Brief Overview of Mizar
- Title not available (Why is that?)
- Untersuchungen über das logische Schliessen. I
- The complexity of theorem-proving procedures
- Hard examples for resolution
- Term Rewriting and All That
- Title not available (Why is that?)
- A machine program for theorem-proving
- HOL Light: An Overview
- On the Computational Complexity of Algebra on Lattices
- Complete Sets of Reductions for Some Equational Theories
- Automatic recognition of tractability in inference relations
- Computer Aided Verification
- Title not available (Why is that?)
- Topological sorting of large networks
- Title not available (Why is that?)
- Free Ortholattices
- Automated complexity analysis based on ordered resolution
- Decision procedures. An algorithmic point of view
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- Proof Complexity
- Free lattices.
- A solution of the uniform word problem for ortholattices
- Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
Cited In (1)
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)
