Name
Abstract | ||
|---|---|---|
If a rewrite-based inference system is guaranteed to terminate on the axioms of a theory T and any set of ground literals, then any theorem-proving strategy based on that inference system is a rewrite-based decision procedure for T-satisfiability. In this paper, we consider the class of theories defining recursive data structures, that might appear out of reach for this approach, because they are defined by an infinite set of axioms. We overcome this obstacle by designing a problem reduction that allows us to prove a general termination result for all these theories. We also show that the theorem-proving strategy decides satisfiability problems in any combination of these theories with other theories decided by the rewrite-based approach. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.entcs.2006.11.039 | Electronic Notes in Theoretical Computer Science (ENTCS) |
Keywords | Field | DocType |
theorem-proving strategy,rewrite-based approach,rewrite-based decision procedure,rewrite-based inference system,inference system,general termination result,ground literal,problem reduction,recursive data structure,satisfiability problem,Recursive Data Structures,Rewrite-Based Satisfiability Procedures | Data structure,Discrete mathematics,Superposition principle,Computer science,Axiom,Satisfiability,Infinite set,Theoretical computer science,Recursion,Inference system,Satisfiability modulo theories | Journal |
Volume | Issue | ISSN |
174 | 8 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
6 | 0.49 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Maria Paola Bonacina | 1 | 544 | 39.48 |
| Mnacho Echenim | 2 | 95 | 15.75 |