scholarly journals Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)

10.29007/7gnr ◽  
2018 ◽  
Author(s):  
Zakaria Chihani ◽  
Dale Miller ◽  
Fabien Renaud
Keyword(s):  
Programming Language ◽  
Logic Program ◽  
Formal Proof ◽  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Backtracking Search ◽  
First Order ◽  
Proof Checker ◽  
Prolog Programming

We present the design philosophy of a proof checker based on a notion of foundational proof certificates. At the heart of this design is a semantics of proof evidence that arises from recent advances in the theory of proofs for classical and intuitionistic logic. That semantics is then performed by a (higher-order) logic program: successful performance means that a formal proof of a theorem has been found. We describe how the lambda Prolog programming language provides several features that help guarantee such a soundness claim. Some of these features (such as strong typing, abstract datatypes, and higher-order programming) were features of the ML programming language when it was first proposed as a proof checker for LCF. Other features of lambda Prolog (such as support for bindings, substitution, and backtracking search) turn out to be equally important for describing and checking the proof evidence encoded in proof certificates. Since trusting our proof checker requires trusting a programming language implementation, we discuss various avenues for enhancing one's trust of such a checker.

Extended natural semantics

1993 ◽  
Vol 3 (2) ◽  
pp. 123-152 ◽  
Author(s):  
John Hannan
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Functional Programming ◽  
Higher Order ◽  
Order Logic ◽  
Inference Rules ◽  
Abstract Syntax ◽  
Higher Order Logic ◽  
First Order ◽  
Definition Of

AbstractWe extend the definition of natural semantics to include simply typed λ-terms, instead of first-order terms, for representing programs, and to include inference rules for the introduction and discharge of hypotheses and eigenvariables. This extension, which we call extended natural semantics, affords a higher-level notion of abstract syntax for representing programs and suitable mechanisms for manipulating this syntax. We present several examples of semantic specifications for a simple functional programming language and demonstrate how we achieve simple and elegant manipulations of bound variables in functional programs. All the examples have been implemented and tested in λProlog, a higher-order logic programming language that supports all of the features of extended natural semantics.

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.

Resolution in type theory

1971 ◽  
Vol 36 (3) ◽  
pp. 414-432 ◽  
Author(s):  
Peter B. Andrews
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Higher Order Logic ◽  
First Order ◽  
Different Types ◽  
Axiomatic Set Theory ◽  
Order Predicate Calculus

In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand's Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.).

scholarly journals Formalization of Linear Space Theory in the Higher-Order Logic Proving System

2013 ◽  
Vol 2013 ◽  
pp. 1-6 ◽  
Author(s):  
Jie Zhang ◽  
Danwen Mao ◽  
Yong Guan
Keyword(s):  
Linear Space ◽  
Theorem Proving ◽  
Predicate Logic ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Space Theory ◽  
Higher Order Logic ◽  
First Order ◽  
Important Approach

Theorem proving is an important approach in formal verification. Higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and stronger semantics. Higher-order logic is more expressive. This paper presents the formalization of the linear space theory in HOL4. A set of properties is characterized in HOL4. This result is used to build the underpinnings for the application of higher-order logic in a wider spectrum of engineering applications.

scholarly journals Antirealism/realism of Hintikka’s game-theoretical semantics

2018 ◽  
Vol 26 (3) ◽  
Author(s):  
Heda Festini
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Higher Order Logic ◽  
First Order ◽  
Theory Of Meaning ◽  
Truth Conditional ◽  
Context Dependent ◽  
Extended Notion

Hintikka’s game-theoretical semantics (GTS) is presented as an anti-Tarskian semantical approach to the context-dependent fragments of Englisch, which overcomes the usual notion of semantical realism. Analysing Hintikka’s critique of Tarski’s interpretation of the truth-conditional theory of meaning, its recursive fashion and the narrow notion of realism, Hintikka’s basic conception is presented in the following manner:1. the Context-Principle vs. the Frege Principle,2.First-order logic together with higher-order logic vs. the primacy of first-order logic,3.verificationist/falsificationist theory vs. Taraski’s narrow truth- conditional theory.Comparing some reviews of Hintikka’s GTS (M. Dummett, E. Itkonen, E. Saarinen, M. Hand) with a short examination of the antirealistic/realistic controversis by C. Wright and M. Dummett, the following was reached:Hintikka’s GTS introduces a new, more extended notion of realism, which embraces Taraski-type realistic semantics, Hintikka’s GTS and with this the question of the possibility to also include Dummett’s neoverificationism or other orientations, remains open.

scholarly journals Making Higher-Order Superposition Work

2021 ◽  
pp. 415-432
Author(s):  
Petar Vukmirović ◽  
Alexander Bentkamp ◽  
Jasmin Blanchette ◽  
Simon Cruanes ◽  
Visa Nummelin ◽  
...  
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Inference Rules ◽  
Higher Order Logic ◽  
First Order ◽  
New Challenges

AbstractSuperposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

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.

Sign in / Sign up

Export Citation Format

Share Document