Constraint solvers are key modules in many systems with reasoning capabilities (e.g., automated theorem provers). To incorporate constraint solvers in such systems, the capability of producing conflict sets or explanations of their results is crucial. For expressiveness, constraints are usually built out in unions of theories and constraint solvers in such unions are obtained by modularly combining solvers for the component theories. In this paper, we consider the problem of modularly constructing conflict sets for a combined theory by re-using available proof-producing procedures for the component theories. The key idea of our solution to this problem is the concept of explanation graph, which is a labelled, acyclic and undirected graph capable of recording the entailment of some equalities. Explanation graphs allow us to record explanations computed by a proof-producing procedure and to refine the Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We also study how the computed conflict sets relate to an appropriate notion of minimality. © Springer-Verlag Berlin Heidelberg 2007.

Combining proof-producing decision procedures / Ranise, S.; Ringeissen, C.; Tran, D. -K.. - 4720:(2007), pp. 237-251. (Intervento presentato al convegno 6th International Symposium on Frontiers of Combining Systems, FroCoS 2007 tenutosi a Liverpool, gbr nel 2007) [10.1007/978-3-540-74621-8_16].

Combining proof-producing decision procedures

Ranise S.;
2007-01-01

Abstract

Constraint solvers are key modules in many systems with reasoning capabilities (e.g., automated theorem provers). To incorporate constraint solvers in such systems, the capability of producing conflict sets or explanations of their results is crucial. For expressiveness, constraints are usually built out in unions of theories and constraint solvers in such unions are obtained by modularly combining solvers for the component theories. In this paper, we consider the problem of modularly constructing conflict sets for a combined theory by re-using available proof-producing procedures for the component theories. The key idea of our solution to this problem is the concept of explanation graph, which is a labelled, acyclic and undirected graph capable of recording the entailment of some equalities. Explanation graphs allow us to record explanations computed by a proof-producing procedure and to refine the Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We also study how the computed conflict sets relate to an appropriate notion of minimality. © Springer-Verlag Berlin Heidelberg 2007.
2007
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-540-74620-1
978-3-540-74621-8
Ranise, S.; Ringeissen, C.; Tran, D. -K.
Combining proof-producing decision procedures / Ranise, S.; Ringeissen, C.; Tran, D. -K.. - 4720:(2007), pp. 237-251. (Intervento presentato al convegno 6th International Symposium on Frontiers of Combining Systems, FroCoS 2007 tenutosi a Liverpool, gbr nel 2007) [10.1007/978-3-540-74621-8_16].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333032
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact