CMU-CS-03-185Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-03-185
Brigitte Pientka December 2003 Ph.D. Thesis
CMU-CS-03-185.ps
Keywords: Logic programming, type theory, automated theorem
proving, logical frameworks
In this thesis, we describe different techniques to improve the overall performance and the expressive power of higher-order logic programming. First, we introduce tabled higher-order logic programming, a novel execution model where some redundant information is eliminated using selective memoization. This extends tabled computation to the higher-order setting and forms the basis of the tabled higher-order logic programming interpreter. Second, we present efficient data-structures and algorithms for higher-order proof search. In particular, we describe a higher-order assignment algorithm which eliminates many unnecessary occurs checks and develop higher-order term indexing. These optimizations are crucial to make tabled higher-order logic programming successful in practice. Finally, we use tabled proof search in the meta-theorem prover to reason efficiently with and about deductive systems. It takes full advantage of higher-order assignment and higher-order term indexing. As experimental results demonstrate, these optimizations taken together constitute a significant step toward exploring the full potential of logical frameworks in practice. 235 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |