Journal of Computer Science

On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey

Sa'ed Abed, Otmane Ait Mohamed and Ghiath Al Sammane

DOI : 10.3844/jcssp.2007.810.817

Journal of Computer Science

Volume 3, Issue 10

Pages 810-817


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.


© 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.