The addition of bounded quantification and partial functions to a computational logic and its theorem prover
| Abstract | 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 | No categories specified (fix it) | |||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,865 |
| External links |
  Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesJö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).
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads3 ( #203,804 of 556,788 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
