Partial Recursive Functions in Higher-Order Logic

2006 ◽  
pp. 589-603 ◽  
Author(s):  
Alexander Krauss
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Recursive Functions ◽  
Partial Recursive Functions

Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod

10.29007/6shf ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Experimental Results ◽  
Relational Model ◽  
Finite Model ◽  
Higher Order Logic ◽  
First Order ◽  
Recursive Functions

Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally a finite model finder, it approximates infinite types by finite subsets. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick generates more counterexamples than other model finders for higher-order logic, without restrictions on the form of the formulas to falsify.

scholarly journals A HOL Basis for Reasoning about Functional Programs

1994 ◽  
Vol 1 (44) ◽  
Author(s):  
Sten Agerholm
Keyword(s):  
Higher Order ◽  
Partial Orders ◽  
Order Logic ◽  
Domain Theory ◽  
Higher Order Logic ◽  
Unification Algorithm ◽  
Recursive Functions ◽  
Bottom Element ◽  
Definition Of ◽  
Primitive Recursive

Domain theory is the mathematical theory underlying denotational semantics. This thesis presents a formalization of domain theory in the Higher Order Logic (HOL) theorem proving system along with a mechanization of proof functions and other tools to support reasoning about the denotations of functional programs. By providing a fixed point operator for functions on certain domains which have a special undefined (bottom) element, this extension of HOL supports the definition of recursive functions which are not also primitive recursive. Thus, it provides an approach to the long-standing and important problem of defining non-primitive recursive functions in the HOL system.<br /> <br />Our philosophy is that there must be a direct correspondence between elements of complete partial orders (domains) and elements of HOL types, in order to allow the reuse of higher order logic and proof infrastructure already available in the HOL system. Hence, we are able to mix domain theoretic reasoning with reasoning in the set theoretic HOL world to advantage, exploiting HOL types and tools directly. Moreover, by mixing domain and set theoretic reasoning, we are able to eliminate almost all reasoning about the bottom element of complete partial orders that makes the LCF theorem prover, which supports a first order logic of domain theory, difficult and tedious to use. A thorough comparison with LCF is provided.<br /> <br />The advantages of combining the best of the domain and set theoretic worlds in the same system are demonstrated in a larger example, showing the correctness of a unification algorithm. A major part of the proof is conducted in the set theoretic setting of higher order logic, and only at a late stage of the proof domain theory is introduced to give a recursive definition of the algorithm, which is not primitive recursive. Furthermore, a total well-founded recursive unification function can be defined easily in pure HOL by proving that the unification algorithm (defined in domain theory) always terminates; this proof is conducted by a non-trivial well-founded induction. In such applications, where non-primitive recursive HOL functions are defined via domain theory and a proof of termination, domain theory constructs only appear temporarily.

scholarly journals Closed Structure

2021 ◽  
Author(s):  
Peter Fritz ◽  
Harvey Lederman ◽  
Gabriel Uzquiano
Keyword(s):  
Formal Language ◽  
Syntactic Structure ◽  
Natural Extension ◽  
Propositional Attitudes ◽  
Higher Order ◽  
Order Logic ◽  
Bertrand Russell ◽  
Structured Propositions ◽  
Higher Order Logic ◽  
Closed Structure

AbstractAccording to the structured theory of propositions, if two sentences express the same proposition, then they have the same syntactic structure, with corresponding syntactic constituents expressing the same entities. A number of philosophers have recently focused attention on a powerful argument against this theory, based on a result by Bertrand Russell, which shows that the theory of structured propositions is inconsistent in higher order-logic. This paper explores a response to this argument, which involves restricting the scope of the claim that propositions are structured, so that it does not hold for all propositions whatsoever, but only for those which are expressible using closed sentences of a given formal language. We call this restricted principle Closed Structure, and show that it is consistent in classical higher-order logic. As a schematic principle, the strength of Closed Structure is dependent on the chosen language. For its consistency to be philosophically significant, it also needs to be consistent in every extension of the language which the theorist of structured propositions is apt to accept. But, we go on to show, Closed Structure is in fact inconsistent in a very natural extension of the standard language of higher-order logic, which adds resources for plural talk of propositions. We conclude that this particular strategy of restricting the scope of the claim that propositions are structured is not a compelling response to the argument based on Russell’s result, though we note that for some applications, for instance to propositional attitudes, a restricted thesis in the vicinity may hold some promise.

Adapting functional programs to higher order logic

2008 ◽  
Vol 21 (4) ◽  
pp. 377-409 ◽  
Author(s):  
Scott Owens ◽  
Konrad Slind
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic

scholarly journals “How did the serpent of inconsistency enter Frege’s paradise?”

2019 ◽  
pp. 411-436
Author(s):  
Crispin Wright
Keyword(s):  
Cardinal Number ◽  
Ordinal Number ◽  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Indefinite Extensibility ◽  
Basic Law ◽  
Per Se

The paper explores the alleged connection between indefinite extensibility and the classic paradoxes of Russell, Burali-Forti, and Cantor. It is argued that while indefinite extensibility is not per se a source of paradox, there is a degenerate subspecies—reflexive indefinite extensibility—which is. The result is a threefold distinction in the roles played by indefinite extensibility in generating paradoxes for the notions of ordinal number, cardinal number, and set respectively. Ordinal number, intuitively understood, is a reflexively indefinitely extensible concept. Cardinal number is not. And Set becomes so only in the setting of impredicative higher-order logic—so that Frege’s Basic Law V is guilty at worst of partnership in crime, rather than the sole offender.

scholarly journals Making Automatic Theorem Provers more Versatile

10.29007/n6j7 ◽  
2018 ◽  
Author(s):  
Simon Cruanes
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Research Directions ◽  
First Order ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.

Sign in / Sign up

Export Citation Format

Share Document