University of Cambridge > > Computer Laboratory Automated Reasoning Group Lunches > LCF-style Propositional Simplification With BDDs and SAT Solvers

LCF-style Propositional Simplification With BDDs and SAT Solvers

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Thomas Tuerk.

I’ll talk about a new way of simplifying the propositional structure of terms in interactive theorem provers. The method uses Binary Decision Diagrams (BDDs) and SAT solvers, but is fully LCF -style. I’ll show how the method improves on standard rewrite-based simplifiers in both a logical and a practical sense.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity