Pubblicazioni

Autori:

Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz

Titolo:

On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal

Anno:

2005

Tipologia prodotto:

Contributo in volume (Capitolo o Saggio)

Tipologia ANVUR:

Contributo in volume (Capitolo o Saggio)

Lingua:

Inglese

Formato:

A Stampa

Titolo libro:

Frontiers of Combining Systems - 5th International Workshop, FroCoS 2005 - Vienna, Austria, September 2005 - Proceedings

Casa editrice:

Springer

ISBN:

9783540290513

Intervallo pagine:

65-80

Parole chiave:

Decision procedures for satisfiability; superposition; rewriting

Breve descrizione dei contenuti:

The rewriting approach to T-satisfiability is based on establishing termination of a rewrite-based inference system for first-order logic on the T-satisfiability problem. Extending previous such results, including the quantifier-free theory of equality and the theory of arrays with or without extensionality, we prove termination for the theories of records with or without extensionality, integer offsets and integer offsets modulo. A general theorem for termination on combinations of theories, that covers any combination of the theories above, is given next. For empirical evaluation, the rewrite-based theorem prover E is compared with the validity checkers CVC and CVC Lite, on both synthetic and real-world benchmarks, including both valid and invalid instances. Parametric synthetic benchmarks test scalability, while real-world benchmarks test ability to handle huge sets of literals. Contrary to the folklore that a general-purpose prover cannot compete with specialized reasoners, the experiments are overall favorable to the theorem prover, showing that the rewriting approach is both elegant and practical.

Pagina Web:

http://dx.doi.org/10.1007/11559306_4
https://mariapaola.github.io/

Id prodotto:

135245

Handle IRIS:

11562/26420

depositato il:

3 dicembre 2007

ultima modifica:

16 settembre 2023

Citazione bibliografica:

Alessandro, Armando; Bonacina, Maria Paola; Silvio, Ranise; Stephan, Schulz, On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal Frontiers of Combining Systems - 5th International Workshop, FroCoS 2005 - Vienna, Austria, September 2005 - Proceedings , 2005 , Springer , 2005 , pp. 65-80

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