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

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

Recommendations

• Reachability programming in HOL98 using BDDs
• Programming a symbolic model checker in a fully expansive theorem prover
• Reflecting BDDs in Coq
• 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)

• Integrating external deduction tools with ACL2
• Reachability programming in HOL98 using BDDs
• Reflecting BDDs in Coq
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• PuzzleTool: An example of programming computation and deduction
• scientific article; zbMATH DE number 834569 (Why is no real title available?)
• LCF-style Platform based on Multiway Decision Graphs

Describes a project that uses

Uses Software

• LCF
• Isabelle

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)