Publications

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

Authors:
Alessandro Armando; Maria Paola Bonacina; 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:
Fifth International Workshop on Frontiers of Combining Systems (FroCoS)
Place:
Vienna, Austria
Period:
September 2005
:
Springer
Publisher:
Springer
ISBN:
9783540290513
Page numbers:
65-80
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; http://profs.sci.univr.it/~bonacina/
Product ID:
26420
Handle IRIS:
11562/26420
Deposited On:
December 3, 2007
Last Modified:
August 28, 2017
Bibliographic citation:
Alessandro Armando; Maria Paola Bonacina; 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 Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (FroCoS)SpringerProceedings of "Fifth International Workshop on Frontiers of Combining Systems (FroCoS)" , Vienna, Austria , September 2005 , 2005pp. 65-80

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