Linking higher order logic to binary decision diagrams

摘要

The ideas described here are intended to provide a platform for experiments in combining deduction and symbolic calculation, such as model checking. The aim is to provide users with a clean logical view based on higher order logic that supports efficient BDD calculations, as provided by BuDDy via MuDDy. Experiments so far suggest that state-of-the-art performance via HOL is attainable and, furthermore, that there are interesting possibilities for combining deduction and symbolic calculation. For example, it is possible to use rewrithing in HOT. to modifv Boolean formulae before converting them to BDDs. This provides a simple high-level method of performing optimisations like early quantification [9, page 45] (or disjunctive partitioning) that avoids the need for tricky BDD programming as well as ensuring soundness.