CMU-CS-00-175Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-00-175
Alberto Momigliano December 2000 Ph.D. Thesis (Philosophy)
CMU-CS-00-175.ps
Keywords: Logical frameworks, higher-order logic programming,
negation, negation-as-failure, strict lambda-calculus, regular
world assumption
Complementing terms, i.e. in our case higher-order patterns. Due the presence of partially applied lambda terms, intuitionistic lambda calculi are not closed under complementation. We thus develop a strict lambda calculus, where we can directly express whether a function depends on its argument. Complementing clauses. This can be seen as a negation normal form procedure which is consistent with intuitionistic provability. It entails finding a middle ground between the Closed World Assumption usually associated with negation and the Open World Assumption typical of logical frameworks. As this is in general not possible, we restrict ourselves to a fragment in which clause complementation is viable and that has proven to be expressive enough for the practice of logical frameworks. The main technical idea is to isolate a set of programs where static and dynamic clauses do not overlap. 166 pages
| |

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