Paper Info
Title
On Variable-inactivity and Polynomial T-Satisfiability Procedures
Abstract
Verification problems require to reason in theories of data structures and fragments of arithmetic. Thus, decision procedures for such theories are needed, to be embedded in, or interfaced with, proof assistants or software model checkers. Such decision procedures ought to be sound and complete, to avoid false negatives and false positives, efficient, to handle large problems, and easy to combine, because most problems involve multiple theories. The rewrite-based approach to decision procedures aims at addressing these sometimes conflicting issues in a uniform way, by harnessing the power of general first-order theorem proving. In this article, we generalize the rewrite-based approach from deciding the satisfiability of sets of ground literals to deciding that of arbitrary ground formulæ in the theory. Next, we present polynomial rewrite-based satisfiability procedures for the theories of records with extensionality and integer offsets. The generalization of the rewrite-based approach to arbitrary ground formulæ and the polynomial satisfiability procedure for the theory of records with extensionality use the same key property—termed variable-inactivity—that allows one to combine theories in a simple way in the rewrite-based approach.
Year
DOI
Venue
2008
10.1093/logcom/exm055
J. Log. Comput.
Keywords
DocType
Volume
theories of data struc- tures,decision procedure,arbitrary ground formul,multiple theory,satis- abilit y modulo theories,theory reasoning,rewrite-based approach,conflicting issue,decision procedures,Polynomial T-Satisfiability Procedures,false positive,polynomial rewrite-based satisfiability procedure,polynomial satisfiability procedure,false negative,rewrite-based theorem-proving,ground literal
Journal
18
Issue
ISSN
Citations 
1
0955-792X
18
PageRank 
References 
Authors
0.66
21
2
Name
Order
Citations
PageRank
Maria Paola Bonacina154439.48
Mnacho Echenim29515.75