Publications

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

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 volume (Capitolo o Saggio)
Tipologia ANVUR:
Contributo in volume (Capitolo o Saggio)
Language:
Inglese
Format:
A Stampa
Book Title:
Frontiers of Combining Systems - 5th International Workshop, FroCoS 2005 - Vienna, Austria, September 2005 - Proceedings
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:
135245
Handle IRIS:
11562/26420
Deposited On:
December 3, 2007
Last Modified:
September 16, 2023
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 Frontiers of Combining Systems - 5th International Workshop, FroCoS 2005 - Vienna, Austria, September 2005 - Proceedings2005Springer2005pp. 65-80

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

<<back

Activities

Research facilities

Share