Title: Theorem proving for untyped constructive -calculus: implementation and application
Abstract: This paper presents a theorem prover for a highly intensional logic, namely a constructive version of property theory [25] (this language essentially provides a combination of constructive first-order logic and the λ-calculus). The paper presents the basic theorem prover, which is a higher-order extension of Manthey and Bry's model generation theorem prover for first-order logic [14]; considers issues relating to the compile-time optimisations that are often used with first-order theorem provers; and shows how the resulting system can be used in a natural language understanding system.
Publication Year: 2001
Publication Date: 2001-01-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 17
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot