Workshop on Automated Reasoning
Bridging the Gap between Theory and Practice

 
 
 

ARW

Background

Call for Papers

Accepted Abstracts

Programme

Venue

Facilities

Accommodation

Travel

Registration

 

Automated Reasoning Workshop 2009
(21st-22nd April 2009, Department of Computer Science, University of Liverpool)

Invited Talk: Konstantin Korovin

Instantiation-based automated reasoning aims to utilise industrial-strength SAT and SMT technologies in the more general context of first-order logic. The basic idea behind instantiation-based reasoning is to combine clever generation of instances with satisfiability checking of ground formulae.

There are a number of challenges arising in this area ranging from theoretical issues such completeness, integration of theories and decidable fragments to efficient implementation: inference strategies, indexing and redundancy elimination. In this talk I will overview the recent advances in instantiation-based reasoning, focusing on a modular approach which allows us to use off-the-shelf SAT and SMT solvers for ground formulae as part of general first-order reasoning.

 
 
 

Maintained by Ullrich Hustadt, U.Hustadt@liverpool.ac.uk, last updated Saturday, 18-Apr-2009 12:03:00 BST.