The addition of bounded quantification and partial functions to a computational logic and its theorem prover
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)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Quantifiers and Congruence Closure.Jörg Flum, Matthias Schiehlen & Jouko Väänänen - 1999 - Studia Logica 62 (3):315-340.
A Logic for Describing, Not Verifying, Software.David Lorge Parnas - 1995 - Erkenntnis 43 (3):321 - 338.
Descriptions in Mathematical Logic.Gerard R. Renardel De Lavalette - 1984 - Studia Logica 43 (3):281 - 294.
A Set Theory with Support for Partial Functions.William M. Farmer & Joshua D. Guttman - 2000 - Studia Logica 66 (1):59-78.
A Mechanization of Strong Kleene Logic for Partial Functions.Manfred Kerber Michael Kohlhase - unknown
Relational and Partial Variable Sets and Basic Predicate Logic.Silvio Ghilardi & Giancarlo Meloni - 1996 - Journal of Symbolic Logic 61 (3):843-872.
Reasoning About Partial Functions with the Aid of a Computer.William M. Farmer - 1995 - Erkenntnis 43 (3):279 - 294.
A Dichotomy in Classifying Quantifiers for Finite Models.Saharon Shelah & Mor Doron - 2005 - Journal of Symbolic Logic 70 (4):1297 - 1324.
Added to index2009-01-28
Total downloads308 ( #9,526 of 2,158,363 )
Recent downloads (6 months)3 ( #133,350 of 2,158,363 )
How can I increase my downloads?