Formula normalizations in verification

DOI10.1007/978-3-031-37709-9_19MaRDI QIDQ6535699zbMATH OpenFDO

Authors Simon Guilloud, Mario Bucev, Dragana Milovančević, Viktor Kuncak

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

Classical propositional logic (03B05) Specification and verification (program logics, model checking, etc.) (68Q60) Free lattices, projective lattices, word problems (06B25)

Recommendations

• Theorem Proving in Higher Order Logics
• Equivalence checking for orthocomplemented bisemilattices in log-linear time
• Normal Forms for Knowledge Compilation
• Simplification of boolean verification conditions
• Short Conjunctive Normal Forms in Finitely Valued Logics

Cites work

• scientific article; zbMATH DE number 3889596 (Why is no real title available?)
• scientific article; zbMATH DE number 758787 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• scientific article; zbMATH DE number 3103212 (Why is no real title available?)
• A Brief Overview of Mizar
• A completion algorithm for lattice tree automata
• A note on orthomodular lattices
• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• Binary decision diagrams
• Boolean Rings for Intersection-Based Satisfiability
• Contract-based resource verification for higher-order functions with memoization
• Decision procedures. An algorithmic point of view
• Equivalence checking for orthocomplemented bisemilattices in log-linear time
• Finitely Presented Lattices
• Free Ortholattices
• Free lattices.
• Function summarization modulo theories
• HOL Light: An Overview
• Implementing Superposition in iProver (System Description)
• Making higher-order superposition work
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• System description: E 1.8
• Term rewrite systems for lattice theory
• The Isabelle Framework

Cited in

(1)

• Equivalence checking for orthocomplemented bisemilattices in log-linear time

This page was built for publication: Formula normalizations in verification

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