Programming Combinations of Deduction and BDD-based Symbolic Calculation

DOI10.1112/S1461157000000693MaRDI QIDQ4827596zbMATH OpenFDO

Authors Michael J. C. Gordon

Publication date 18 November 2004

Published in LMS Journal of Computation and Mathematics (Search for Journal in Brave)

Full work available at URL http://www.lms.ac.uk/jcm/5/lms2000-001/

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1670743
• Programming a symbolic model checker in a fully expansive theorem prover
• scientific article; zbMATH DE number 1696436
• Automated Deduction with Shannon Graphs
• Extended Resolution Proofs for Conjoining BDDs

Cites work

• A theory of type polymorphism in programming
• Interpolants and Symbolic Model Checking

Cited in

(7)

• LCF-style Platform based on Multiway Decision Graphs
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• Integrating external deduction tools with ACL2
• scientific article; zbMATH DE number 1670743 (Why is no real title available?)
• scientific article; zbMATH DE number 834569 (Why is no real title available?)
• scientific article; zbMATH DE number 1927424 (Why is no real title available?)
• scientific article; zbMATH DE number 1696436 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle
• LCF

This page was built for publication: Programming Combinations of Deduction and BDD-based Symbolic Calculation

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