Publications

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:

Sì

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
https://mariapaola.github.io/

Product ID:

30956

Handle IRIS:

11562/30956

Deposited On:

November 5, 2007

Last Modified:

September 16, 2023

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) , Elsevier , Proceedings 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 , 2007 , pp. 55-70

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