scholarly journals Graph Representations for Higher-Order Logic and Theorem Proving

2020 ◽  
Vol 34 (03) ◽  
pp. 2967-2974
Author(s):  
Aditya Paliwal ◽  
Sarah Loos ◽  
Markus Rabe ◽  
Kshitij Bansal ◽  
Christian Szegedy
Keyword(s):  
Theorem Proving ◽  
State Of The Art ◽  
Higher Order ◽  
Order Logic ◽  
Established Method ◽  
Higher Order Logic ◽  
Graph Representations ◽  
Significant Challenge ◽  
Proof Search ◽  
Graph Neural Networks

This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem provers allow for the formalization of most mathematical theories and have been shown to pose a significant challenge for deep learning. Higher-order logic is highly expressive and, even though it is well-structured with a clearly defined grammar and semantics, there still remains no well-established method to convert formulas into graph-based representations. In this paper, we consider several graphical representations of higher-order logic and evaluate them against the HOList benchmark for higher-order theorem proving.

scholarly journals Extending a brainiac prover to lambda-free higher-order logic

2021 ◽  
Author(s):  
Petar Vukmirović ◽  
Jasmin Blanchette ◽  
Simon Cruanes ◽  
Stephan Schulz
Keyword(s):  
Data Structures ◽  
Theorem Proving ◽  
State Of The Art ◽  
Higher Order ◽  
The State ◽  
Order Logic ◽  
Automatic Theorem Proving ◽  
Higher Order Logic ◽  
First Order ◽  
Automatic Theorem

AbstractDecades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to $$\lambda $$ λ -free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone toward full higher-order logic.

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 Toward the Formalization of Macroscopic Models of Traffic Flow Using Higher-Order-Logic Theorem Proving

IEEE Access ◽  
2020 ◽  
Vol 8 ◽  
pp. 27291-27307
Author(s):  
Adnan Rashid ◽  
Muhammad Umair ◽  
Osman Hasan ◽  
Mohamed H. Zaki
Keyword(s):  
Traffic Flow ◽  
Theorem Proving ◽  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Macroscopic Models

Probabilistic Analysis Using Theorem Proving

2015 ◽  
pp. 21-28
Keyword(s):  
Model Checking ◽  
Theorem Proving ◽  
Probabilistic Analysis ◽  
Probabilistic Model ◽  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Probabilistic Model Checking ◽  
Higher Order Logic ◽  
Comprehensive Framework

In this chapter, the authors first provide the overall methodology for the theorem proving formal probabilistic analysis followed by a brief introduction to the HOL4 theorem prover. The main focus of this book is to provide a comprehensive framework for formal probabilistic analysis as an alternative to less accurate techniques like simulation and paper-and-pencil methods and to other less scalable techniques like probabilistic model checking. For this purpose, the HOL4 theorem prover, which is a widely used higher-order-logic theorem prover, is used. The main reasons for this choice include the availability of foundational probabilistic analysis formalizations in HOL4 along with a very comprehensive support for real and set theoretic reasoning.

Sign in / Sign up

Export Citation Format

Share Document