LCF-Style Propositional Simplification with BDDs and SAT Solvers

DOI10.1007/978-3-540-71067-7_9zbMath1165.68443OpenAlexW1549391871MaRDI QIDQ3543649

Hasan Amjad

Publication date: 4 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71067-7_9

Mathematics Subject Classification ID

Uses Software

• Coq
• MiniSat
• ML
• PVS
• HOL
• Chaff

Cites Work

• Efficiently checking propositional refutations in HOL theorem provers
• Isabelle. A generic theorem prover
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: LCF-Style Propositional Simplification with BDDs and SAT Solvers