Publications

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

Authors:
BONACINA, Maria Paola; ECHENIM, Bertrand Mnacho
Title:
Rewrite-based satisfiability procedures for recursive data structures
Year:
2007
Type of item:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Language:
Inglese
Format:
Elettronico
Referee:
Name of journal:
Electronic Notes in Theoretical Computer Science
ISSN of journal:
1571-0661
N° Volume:
174
Number or Folder:
8
Congresso:
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)
Place:
Seattle, WA, U.S.A.
Period:
August 2006
:
Elsevier
Publisher:
Elsevier
Page numbers:
55-70
Keyword:
Satisfiability modulo theories; rewrite-based theorem proving; superposition
Short description of contents:
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)
Web page:
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
Product ID:
30956
Handle IRIS:
11562/30956
Deposited On:
November 5, 2007
Last Modified:
June 30, 2020
Bibliographic citation:
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)ElsevierProceedings of "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

Related projects
Title Department Managers
Sintesi di procedure di decisione basate sulla deduzione con applicazioni all'analisi formale automatica di programmi (PRIN 2003) Department Informatica Maria Paola Bonacina
<<back

Activities

Research facilities