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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

LCF-style Propositional Simplification With BDDs and SAT Solvers

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Cambridge BSU Lectures in Biomedical Data Science Lennard-Jones Centre New Exam Study

Other talks

Synthesizing Diverse Policies for Multi-Agent Coordination Strange New Worlds Online Causal Inference Seminar Title to be confirmed An AI-Assisted Proof in Spectral Geometry Polar Oceans Seminar Talk
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity