The rewrite-based approach to satisfiability modulo theories consists of using generic theorem-proving strategies for first-order logic with equality. If one can prove that the considered inference system generates finitely many clauses from the presentation T of a theory and a finite set of ground unit clauses, then any fair strategy can be used as a T-satisfiability procedure. This approach makes it conceptually simple to combine several theories, under the variable-inactive condition. In this paper, we introduce sufficient conditions to generalize the entire framework of rewrite-based T-satisfiability procedures to rewrite-based T-decision procedures. These conditions, collectively termed as subterm-inactivity, will allow us to obtain rewrite-based T-decision procedures for several theories, namely those of equality with uninterpreted functions, arrays with or without extensionality and two of its extensions, finite sets with extensionality and recursive data structures. We show that subterm-inactive theories are also variable-inactive, and can therefore all be combined.
Rewrite-based decision procedures
BONACINA, Maria Paola;ECHENIM, Bertrand Mnacho
2007-01-01
Abstract
The rewrite-based approach to satisfiability modulo theories consists of using generic theorem-proving strategies for first-order logic with equality. If one can prove that the considered inference system generates finitely many clauses from the presentation T of a theory and a finite set of ground unit clauses, then any fair strategy can be used as a T-satisfiability procedure. This approach makes it conceptually simple to combine several theories, under the variable-inactive condition. In this paper, we introduce sufficient conditions to generalize the entire framework of rewrite-based T-satisfiability procedures to rewrite-based T-decision procedures. These conditions, collectively termed as subterm-inactivity, will allow us to obtain rewrite-based T-decision procedures for several theories, namely those of equality with uninterpreted functions, arrays with or without extensionality and two of its extensions, finite sets with extensionality and recursive data structures. We show that subterm-inactive theories are also variable-inactive, and can therefore all be combined.File | Dimensione | Formato | |
---|---|---|---|
STRAT-FLOC2006gendp.pdf
accesso aperto
Descrizione: Articolo
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
344.58 kB
Formato
Adobe PDF
|
344.58 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.