Publications

Authors:

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

Title:

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

Year:

2005

Type of item:

Contributo in atti di convegno

Tipologia ANVUR:

Contributo in Atti di convegno

Language:

Inglese

Format:

A Stampa

Name of journal:

Lecture Notes in Artificial Intelligence

N° Volume:

3717

Congresso:

International Workshop on Frontiers of Combining Systems

Place:

Vienna, Austria

Period:

September 2005

:

Springer

Publisher:

Springer

ISBN:

9783540290513

Page numbers:

65-80

Keyword:

Decision procedures for satisfiability; superposition; rewriting

Short description of contents:

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.

Web page:

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

Product ID:

150025

Handle IRIS:

11562/26420

Deposited On:

December 3, 2007

Last Modified:

February 25, 2026

Bibliographic citation:

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

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