University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Finite Model Generation, Proof-Producing SAT Solvers, and SMT

  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

Finite Model Generation, Proof-Producing SAT Solvers, and SMT

Download to your calendar using vCal

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

This talk consists of three parts. First, I will present a finite model generator for higher-order logic. The input formula is translated to propositional logic, so that a standard SAT solver can be employed for the actual model search. The model generator supports many of the definitional mechanisms available in the Isabelle/HOL theorem prover, and has been applied to various case studies.

Second, I will present an integration of proof-producing SAT solvers with higher-order logic theorem provers. An adequate representation of the SAT problem allows to verify unsatisfiability proofs with millions of resolutions steps.

Last, I will give a brief introduction to Satisfiability Modulo Theories (SMT), the decision problem for first-order formulae with respect to combinations of background theories.

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

This seminar will be held in a hybrid format at MR 12, Centre of Mathematical Sciences, CB3 0WA. Alternatively you can also join with Zoom (see abstract for Zoom link). The Centre For Financial Analysis & Policy Webinar & LT2, Computer Laboratory, William Gates Building.

Other talks

Group Work Tea and Coffee Break Talk title TBC  Life, death, and the discovery of PDAR: the Pol II Degradation-dependent Apoptotic Response  Group Work Filial Lines: Art Spiegelman, Alison Bechdel, and Comics Form
 

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