Deduction, strategies, and rewriting

In M. Archer, T. B. de la Tour, and C. A. Muñoz, editors, 6th International Workshop on Strategies in Automated Deduction, STRATEGIES'06, Seattle, Washington, August 16, 2006, Part of FLOC 2006, ENTCS 174(10), pages 119-137. Elsevier, 2007.

Abstract: Automated deduction methods should be specified not procedurally, but declaratively, as inference systems which are proved correct regardless of implementation details. Then, different algorithms to implement a given inference system should be specified as strategies to apply the inference rules. The inference rules themselves can be naturally specified as (possibly conditional) rewrite rules. Using a high-performance rewriting language implementation and a strategy language to guide rewriting computations, we can obtain in a modular way implementations of both the inference rules of automated deduction procedures and of algorithms controling their application. This paper presents the design of a strategy language for the Maude rewriting language that supports this modular decomposition: inference systems are specified in system modules, and strategies in strategy modules. We give a set-theoretic semantics for this strategy language, present its different combinators, illustrate its main ideas with several examples, and describe both a reflective prototype in Maude and an ongoing C++ implementation.

[pdf]

@inproceedings{strategies06,
	Author = {Steven Eker and Narciso Mart\'{\i}-Oliet and Jos{\'\e} Meseguer and Alberto Verdejo},
	Title = {Deduction, Strategies, and Rewriting},
	Booktitle = {6th International Workshop on Strategies in Automated Deduction, 
	             STRATEGIES'06, Seattle, Washington, August 16, 2006, Part of FLOC 2006},
	Editor = {M. Archer and T. Boy de la Tour and C. A. Mu\~noz},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Number = {11},
	Volume = {174},
	Pages = {3-25},
	Year = {2007}}