Loading...
Please wait, while we are loading the content...
Similar Documents
A Logic Programming Approach To Manipulating Formulas And Programs (1994)
| Content Provider | CiteSeerX |
|---|---|
| Author | Miller, Dale Nadathur, Gopalan |
| Description | IEEE Symp. Logic Programming : First-order Horn clause logic can be extended to a higher-order setting in which function and predicate symbols can be variables and terms are replaced with simply typed -terms. For such a logic programming language to be complete in principle, it must incorporate higher-order unification. Although higher-order unification is more complex than usual first-order unification, its availability makes writing certain kinds of programs far more straightforward. In this paper, we present such programs written in a higherorder version of Prolog called Prolog. These programs manipulate structures, such as formulas and programs, which contain abstractions or bound variables. We show how a simple natural deduction theorem prover can be implemented in this language. Similarly we demonstrate how several simple program transformers for a functional programming language can be written in Prolog. These Prolog programs exploit the availability of -conversion and higher-order unification to elegantly ... |
| File Format | |
| Language | English |
| Publisher Date | 1994-01-01 |
| Access Restriction | Open |
| Subject Keyword | Prolog Program Logic Programming Language First-order Horn Clause Logic Higher-order Setting Several Simple Program Transformer Functional Programming Language Logic Programming Approach Bound Variable Higherorder Version Simple Natural Deduction Theorem Prover Usual First-order Unification Certain Kind Manipulating Formula Predicate Symbol Typed Term Higher-order Unification |
| Content Type | Text |
| Resource Type | Article |
