Many applications of automated reasoning require decision procedures for the satisfiability of a formula in a theory given by the union of a few theories. Reasoning in a union of theories can be approached in more than one way. The equality-sharing method, also known as Nelson-Oppen scheme, combines decision procedures for the component theories. Superposition-based theorem-proving strategies unite the presentations of the theories to reason about their union. CDSAT, which stands for Conflict-Driven SATisfiability, assumes that each theory is equipped with an inference system, called theory module, and coordinates the theory modules to reason in a conflict-driven manner in the union of the theories. A theory module is an abstraction of a decision procedure, made of inference rules that may correspond to axioms of the theory. Conflict-driven means that the system maintains a representation of a candidate partial model of the formula, and performs nontrivial inferences only to explain conflicts between the candidate model and the formula, so that the conflict can be solved by updating the partial model. CDSAT provides a framework where the theory modules cooperate to build the candidate model and to explain the conflicts. This talk presents CDSAT placing it in the big picture of multi-theory reasoning and conflict-driven reasoning.

Conflict-driven reasoning in unions of theories

Maria Paola Bonacina
2019-01-01

Abstract

Many applications of automated reasoning require decision procedures for the satisfiability of a formula in a theory given by the union of a few theories. Reasoning in a union of theories can be approached in more than one way. The equality-sharing method, also known as Nelson-Oppen scheme, combines decision procedures for the component theories. Superposition-based theorem-proving strategies unite the presentations of the theories to reason about their union. CDSAT, which stands for Conflict-Driven SATisfiability, assumes that each theory is equipped with an inference system, called theory module, and coordinates the theory modules to reason in a conflict-driven manner in the union of the theories. A theory module is an abstraction of a decision procedure, made of inference rules that may correspond to axioms of the theory. Conflict-driven means that the system maintains a representation of a candidate partial model of the formula, and performs nontrivial inferences only to explain conflicts between the candidate model and the formula, so that the conflict can be solved by updating the partial model. CDSAT provides a framework where the theory modules cooperate to build the candidate model and to explain the conflicts. This talk presents CDSAT placing it in the big picture of multi-theory reasoning and conflict-driven reasoning.
2019
978-3-030-29007-8
Satisfiability modulo theories, Satisfiability modulo assignments, Theory Combination
File in questo prodotto:
File Dimensione Formato  
twopages.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 127.83 kB
Formato Adobe PDF
127.83 kB Adobe PDF Visualizza/Apri

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/11562/996425
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact