Journal article
Cooperation of background reasoners in theory reasoning by residue sharing
Journal of automated reasoning, Vol.30(1), pp.1-31
01/01/2003
DOI: 10.1023/A:1022587501759
Abstract
We propose a general way of combining background reasoners in theory reasoning. Using a restricted version of the Craig interpolation lemma, we show that background reasoner cooperation can be achieved as a form of constraint propagation, much in the spirit of existing combination methods for decision procedures. In this case, constraint information is propagated across reasoners eexchanging residues that are, in essence, disjunctions of ground literals over a common signature. As an application of our approach, we describe a multitheory version of the semantic tableau calculus, and we prove it sound and complete.
Details
- Title: Subtitle
- Cooperation of background reasoners in theory reasoning by residue sharing
- Creators
- C Tinelli - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Journal of automated reasoning, Vol.30(1), pp.1-31
- Publisher
- Springer Nature
- DOI
- 10.1023/A:1022587501759
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- Number of pages
- 31
- Language
- English
- Date published
- 01/01/2003
- Academic Unit
- Computer Science
- Record Identifier
- 9984259492902771
Metrics
4 Record Views