MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Combination of disjoint theories: beyond decidability

Pascal Fontaine
INRIA Nancy
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
MPI Audience
English

Date, Time and Location

Wednesday, 21 March 2012
10:00
60 Minutes
E1 4
019
Saarbrücken

Abstract

Combination of theories underlies the design of satisfiability modulo theories (SMT) solvers.

The Nelson-Oppen framework can be used to build a decision procedure for the combination
of two disjoint decidable stably infinite theories.

We study the more general case of combining theories for which there exist refutationally complete
procedures. We consider two cases and provide complete (semi-)algorithms for them. First, we
show that it is possible under minor technical conditions to combine a decidable
(not necessarily stably infinite) theory and a disjoint finitely axiomatize theory, obtaining a refutationally
complete procedure. Second, we provide a refutationally complete procedure for the union of two
disjoint finitely axiomatized theories, that uses the assumed procedures for the underlying theories without
modifying them.

(Joint work with Stephan Merz and Christoph Weidenbach)

Contact

Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only

Jennifer Müller, 03/13/2012 09:49 -- Created document.