Loading...
Please wait, while we are loading the content...
Similar Documents
A Logic Programming Approach to Implementing Higher-Order Term Rewriting (1992)
| Content Provider | CiteSeerX |
|---|---|
| Author | Felty, Amy |
| Description | Term rewriting has proven to be an important technique in theorem proving. In this paper, we illustrate that rewrite systems and strategies for higher-order term rewriting, which includes the usual notion of first-order rewriting, can be naturally specified and implemented in a higher-order logic programming language. We adopt a notion of higher-order rewrite system which uses the simply typed -calculus as the language for expressing rules, with a restriction on the occurrences of free variables on the left hand sides of rules so that matching of terms with rewrite templates is decidable. The logic programming language contains an implementation of the simply-typed lambda calculus including fij- conversion and higher-order unification. In addition, universal quantification in queries and the bodies of clauses is permitted. For higher-order rewriting, we show how these operations implemented at the meta-level provide elegant mechanisms for the object-level operations of descending thro... |
| File Format | |
| Language | English |
| Publisher | Springer-Verlag |
| Publisher Date | 1992-01-01 |
| Publisher Institution | Second International Workshop on Extensions to Logic Programming, volume 596 of Lecture Notes in Arti Intelligence |
| Access Restriction | Open |
| Subject Keyword | Left Hand Side Typed Calculus Theorem Proving Meta-level Provide Elegant Mechanism Higher-order Logic Programming Language Universal Quantification Rewrite Template Usual Notion Important Technique Free Variable First-order Rewriting Higher-order Term Rewriting Object-level Operation Logic Programming Language Higher-order Rewrite System Rewrite System Logic Programming Approach Fij Conversion Implementing Higher-order Term Rewriting Simply-typed Lambda Calculus Term Rewriting Higher-order Rewriting Higher-order Unification |
| Content Type | Text |
| Resource Type | Article |