Pubblicazioni

Rewrite-based satisfiability procedures for recursive data structures  (2007)

Autori:
BONACINA, Maria Paola; ECHENIM, Bertrand Mnacho
Titolo:
Rewrite-based satisfiability procedures for recursive data structures
Anno:
2007
Tipologia prodotto:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Lingua:
Inglese
Formato:
Elettronico
Referee:
Nome rivista:
Electronic Notes in Theoretical Computer Science
ISSN Rivista:
1571-0661
N° Volume:
174
Numero o Fascicolo:
8
Titolo del Convegno:
Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Third International Joint Conference on Automated Reasoning (IJCAR) and Fourth Federated Logic Conference (FLoC)
Luogo:
Seattle, WA, U.S.A.
Periodo:
August 2006
Editore:
Elsevier
Casa editrice:
Elsevier
Intervallo pagine:
55-70
Parole chiave:
Satisfiability modulo theories; rewrite-based theorem proving; superposition
Breve descrizione dei contenuti:
If a rewrite-based inference system is guaranteed to terminate on the axioms of a theory T and any set of ground literals, then any theorem-proving strategy based on that inference system is a rewrite-based decision procedure for T-satisfiability. In this paper, we consider the class of theories defining recursive data structures, that might appear out of reach for this approach, because they are defined by an infinite set of axioms. We overcome this obstacle by designing a problem reduction that allows us to prove a general termination result for all these theories. We also show that the theorem-proving strategy decides satisfiability problems in any combination of these theories with other theories decided by the rewrite-based approach.
Note:
The Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) was a satellite of the Third International Joint Conference on Automated Reasoning (IJCAR) at the Fourth Federated Logic Conference (FLoC)
Pagina Web:
http://doi.org/10.1016/j.entcs.2006.11.039; http://profs.sci.univr.it/~bonacina/rewsat.html; http://profs.sci.univr.it/~bonacina/worksbydate.html; http://profs.sci.univr.it/~bonacina/pub_conf.html
Id prodotto:
30956
Handle IRIS:
11562/30956
depositato il:
5 novembre 2007
ultima modifica:
30 giugno 2020
Citazione bibliografica:
BONACINA, Maria Paola; ECHENIM, Bertrand Mnacho, Rewrite-based satisfiability procedures for recursive data structures in «Electronic Notes in Theoretical Computer Science» vol. 174 n. 8 Elsevier  in Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR)ElsevierAtti di "Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Third International Joint Conference on Automated Reasoning (IJCAR) and Fourth Federated Logic Conference (FLoC)" , Seattle, WA, U.S.A. , August 2006 , 2007pp. 55-70

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

Progetti Collegati
Titolo Dipartimento Responsabili
Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003) Dipartimento Informatica Maria Paola Bonacina
<<indietro

Attività

Strutture