Oliver Kullmann,

University of Wales Swansea –

Abstract:

I want to present some joint work with Joao Marques-Silva and
Ines Lynce on the problem of finding “good” unsatisfiable sub-clause-sets
of some given unsatisfiable clause-set. This problem has
applications in consistency checking of order specifications as well
as in model checking.

Our approach is based on a fine-grained analysis of the clause-set,
exploiting proof-theoretical and semantical properties. Especially the
analysis of minimally unsatisfiable sub-clause-sets and generalisations
to “lean” clause-sets (i.e., “autarky-free” clause-sets) will play a role
here.

 

Date: 2006-May-16     Time: 14:00:00     Room: 217

For more information: