de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45635

Tran,  Duc-Khanh
Automation of Logic, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Tran, D.-K., Ringeissen, C., Ranise, S., & Kirchner, H. (2010). Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation. Journal of Symbolic Computation, 45(2), 261-268. doi:doi:10.1016/j.jsc.2008.10.006.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-1A46-E
Abstract
Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple ``sat/unsat'' answer. In this paper, we develop a framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the framework to specify and prove the correctness of classic combination schemas by Nelson-Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them for large classes of theories, then we provide a schema to modularly combine them. Third, we consider the problem of modularly constructing explanations for combinations by re-using available proof-producing procedures for the component theories.