scholarly journals Isabelle’s Metalogic: Formalization and Proof Checker

2021 ◽  
pp. 93-110
Author(s):  
Tobias Nipkow ◽  
Simon Roßkopf
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
Proof Checker ◽  
Proof Terms

AbstractIsabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.

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.

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.

scholarly journals Leo-III Version 1.1 (System description)

10.29007/grmx ◽  
2018 ◽  
Author(s):  
Christoph Benzmüller ◽  
Alexander Steen ◽  
Max Wisniewski
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
System Description ◽  
Agent Based ◽  
First Order ◽  
Theorem Provers ◽  
Automated Theorem Prover ◽  
Ordering Constraints

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external first-order theorem provers.Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III's underlying calculus, survey implementation details and give examples of use.

scholarly journals A Mechanised Semantics for HOL with Ad-hoc Overloading

10.29007/413d ◽  
2020 ◽  
Author(s):  
Johannes Åman Pohjola ◽  
Arve Gengelbach
Keyword(s):  
Ad Hoc ◽  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic

Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions— that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with ad-hoc overloading is consistent. All our results have been formalised in the HOL4 theorem prover.

scholarly journals Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic

10.29007/dzc2 ◽  
2018 ◽  
Author(s):  
Max Wisniewski ◽  
Alexander Steen
Keyword(s):  
Modal Logic ◽  
Higher Order ◽  
Order Logic ◽  
Tense Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
First Order ◽  
Automated Theorem Prover ◽  
Nominal Logic ◽  
The Moment

In this paper, we present an embedding of higher-order nominal modal logicinto classical higher-order logic, and study its automation. There exists no automated theorem prover for first-order or higher-order nominal logic at the moment, hence, this is the first automation for this kind of logic.In our work, we focus on nominal tense logic and have successfully proven some first theorems.

scholarly journals Formal verification of Matrix based MATLAB models using interactive theorem proving

2021 ◽  
Vol 7 ◽  
pp. e440
Author(s):  
Ayesha Gauhar ◽  
Adnan Rashid ◽  
Osman Hasan ◽  
João Bispo ◽  
João M.P. Cardoso
Keyword(s):  
Formal Verification ◽  
Finite Impulse Response ◽  
Formal Analysis ◽  
Digital Signal ◽  
Interactive Theorem Proving ◽  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Formal Models ◽  
Higher Order Logic

MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.

scholarly journals Going Polymorphic - TH1 Reasoning for Leo-III

10.29007/jgkw ◽  
2018 ◽  
Author(s):  
Alexander Steen ◽  
Max Wisniewski ◽  
Christoph Benzmüller
Keyword(s):  
Type Systems ◽  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Proof Assistants ◽  
Interactive Proof ◽  
Higher Order Logic ◽  
Theorem Provers ◽  
Reasoning System ◽  
Automated Theorem Prover

While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed lambda-calculi and therefore do not allow such flexibility. In this paper, we present modifications to the higher-order automated theorem prover Leo-III for turning it into a reasoning system for rank-1 polymorphic HOL.To that end, a polymorphic version of HOL and a suitable paramodulation-based calculus are sketched. The implementation is evaluated using a set of polymorphic TPTP THF problems.

Sign in / Sign up

Export Citation Format

Share Document