On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey
Abstract
This survey discuss approaches that integrate Decision Diagrams inside High Order Logic based Theorem provers. The approaches can be divided in two kinds, one is based on building a translation between model checker and theorem prover, the second is based on embedding the model checker algorithms inside the theorem prover. A comparison between both is discussed in detail. The paper also tries to answer which is the best decision graphs formalization for theorem provers as what is the optimized set of operations to efficiently manipulate the decision graphs inside theorem provers. Then, we contrast between them according to their efficiency, complexity and feasibility.
DOI: https://doi.org/10.3844/jcssp.2007.810.817
Copyright: © 2007 Sa'ed Abed, Otmane Ait Mohamed and Ghiath Al Sammane. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
- 3,249 Views
- 2,328 Downloads
- 0 Citations
Download
Keywords
- Model checking
- theorem proving
- hybrid approach
- deep embedding
- logical representation
- graphical representation