Programming Combinations of Deduction and BDD-based Symbolic Calculation

DOI10.1112/S1461157000000693zbMATH Open1068.68682MaRDI QIDQ4827596FDOQ4827596

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/

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

Mathematics Subject Classification ID

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

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
• Title not available (Why is that?)
• Integrating external deduction tools with ACL2
• Title not available (Why is that?)
• Title not available (Why is that?)
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• Title not available (Why is that?)

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)