Research Article Open Access

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

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.

Journal of Computer Science
Volume 3 No. 10, 2007, 810-817

DOI: https://doi.org/10.3844/jcssp.2007.810.817

Submitted On: 19 August 2007 Published On: 31 October 2007

How to Cite: Abed, S., Mohamed, O. A. & Sammane, G. A. (2007). On The Integration of Decision Diagrams in High Order Logic Based Theorem Provers: a Survey . Journal of Computer Science, 3(10), 810-817. https://doi.org/10.3844/jcssp.2007.810.817

  • 2,687 Views
  • 2,036 Downloads
  • 0 Citations

Download

Keywords

  • Model checking
  • theorem proving
  • hybrid approach
  • deep embedding
  • logical representation
  • graphical representation