Prototyping Completion with Constraints Using Computational Systems

13 years 11 months ago
Prototyping Completion with Constraints Using Computational Systems
We use computational systems to express a completion with constraints procedure that gives priority to simplifications. Computational systems are rewrite theories enriched by strategies. The implementation of completion in ELAN, an interpretor of computational systems, is especially convenient for experimenting with different simplification strategies, thanks to the powerful strategy language of ELAN. 1 Motivations Completion procedures, as many computational processes, can be formulated as instances of a schema that consists of applying rewrite rules on formulas with some strategy, until getting specific normal forms. In this sense they can be understood as computational systems [1], i.e. rewrite theories in rewriting logic, enriched by a notion of strategy for selecting interesting derivations. Symbolic constraint solvers can also be described by computational systems that rewrite constraints to their solved forms. Putting together completion and constraint solving rules leads to...
Hélène Kirchner, Pierre-Etienne More
Added 26 Aug 2010
Updated 26 Aug 2010
Type Conference
Year 1995
Where RTA
Authors Hélène Kirchner, Pierre-Etienne Moreau
Comments (0)