The addition of bounded quantification and partial functions to a computational logic and its theorem prover
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
We describe an extension to our quantifier-free computational logic to provide the expressive power and convenience of bounded quantifiers and partial functions. By quantifier we mean a formal construct which introduces a bound or indicial variable whose scope is some subexpression of the quantifier expression. A familiar quantifier is the Σ operator which sums the values of an expression over some range of values on the bound variable. Our method is to represent expressions of the logic as objects in the logic, to define an interpreter for such expressions as a function in the logic, and then define quantifiers as "mapping functions." The novelty of our approach lies in the formalization of the interpreter and its interaction with the underlying logic. Our method has several advantages over other formal systems that provide quantifiers and partial functions in a logical setting. The most important advantage is that proofs not involving quantification or partial recursive functions are not complicated by such notions as "capturing," "bottom," or "continuity." Naturally enough, our formalization of the partial functions is nonconstructive. The theorem prover for the logic has been modified to support these new features. We describe the modifications. The system has proved many theorems that could not previously be stated in our logic. Among them are.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Jörg Flum, Matthias Schiehlen & Jouko Väänänen (1999). Quantifiers and Congruence Closure. Studia Logica 62 (3):315-340.
David Lorge Parnas (1995). A Logic for Describing, Not Verifying, Software. Erkenntnis 43 (3):321 - 338.
Gerard R. Renardel De Lavalette (1984). Descriptions in Mathematical Logic. Studia Logica 43 (3):281 - 294.
William M. Farmer & Joshua D. Guttman (2000). A Set Theory with Support for Partial Functions. Studia Logica 66 (1):59-78.
Silvio Ghilardi & Giancarlo Meloni (1996). Relational and Partial Variable Sets and Basic Predicate Logic. Journal of Symbolic Logic 61 (3):843-872.
William M. Farmer (1995). Reasoning About Partial Functions with the Aid of a Computer. Erkenntnis 43 (3):279 - 294.
Saharon Shelah & Mor Doron (2005). A Dichotomy in Classifying Quantifiers for Finite Models. Journal of Symbolic Logic 70 (4):1297 - 1324.
Gerard R. Renardel de Lavalette (1984). Descriptions in Mathematical Logic. Studia Logica 43 (3):281-294.
Added to index2009-01-28
Total downloads303 ( #6,797 of 1,796,210 )
Recent downloads (6 months)45 ( #19,624 of 1,796,210 )
How can I increase my downloads?