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...

• Type: Conference
• Year: 1995
• Where: RTA
• Authors: Hélène Kirchner, Pierre-Etienne Moreau
• Keywords: Computational Systems, Motivations Completion Procedures, Rewrite Theories, RTA 1995, Theoretical Computer Science