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

Cambridge users (raven)details Other usersdetails No account?details

Information on

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

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.

Other lists

Discrete Analysis Seminar Sustainability Talks EDC Inclusive design

Other talks

TBC The genetic framework of germline stem cell development My ceramic practice, and Moon Jars for the 21st century Dive into the Lives of Flies and Ants Oncological Imaging: introduction and non-radionuclide techniques & radionuclide techniques Bayesian optimal design for Gaussian process model 'Cryptocurrency and BLOCKCHAIN – PAST, PRESENT AND FUTURE' The Productivity Paradox: are we too busy to get anything done? LARMOR LECTURE - Exoplanets, on the hunt of Universal life Sneks long balus Retinal mechanisms of non-image-forming vision The Age of the Applied Economist: The Transformation of Economics Since the 1970s
 

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