CADE
2010
Springer
13 years 10 months ago
2010
Springer
x-free and employs a novel clausal form that abstracts away from propositional reasoning. It comes with an elegant correctness proof. We discuss some optimizations for decision pro...
CADE
2010
Springer
13 years 10 months ago
2010
Springer
WRLA
2010
13 years 10 months ago
2010
This paper presents the main results and conclusions of the Third Rewrite Engines Competition (REC III). This edition of the competition took place as part of the 8th Workshop on R...
WRLA
2010
13 years 10 months ago
2010
WRLA
2010
13 years 10 months ago
2010
WRLA
2010
13 years 10 months ago
2010
Abstract. If a set of equations E∪Ax is such that E is confluent, terminating, and coherent modulo Ax, narrowing with E modulo Ax provides a complete E∪Ax-unification algorit...
WRLA
2010
13 years 10 months ago
2010
Abstract. We revise multiset rewriting with name binding, by combining the two main existing approaches to the study of concurrency by means of multiset rewriting, multiset rewriti...
WRLA
2010
13 years 10 months ago
2010
For a rewrite theory to be executable, its equations E should be (ground) confluent and terminating modulo the given axioms A, and their rules should be (ground) coherent with E m...
WRLA
2010
13 years 10 months ago
2010
Abstract. This paper presents the foundation, design, and implementation of the Linear Temporal Logic of Rewriting model checker as an extension of the Maude system. The Linear Tem...
CADE
2010
Springer
13 years 10 months ago
2010
Springer
