scholarly journals Composable Packages for Higher Order Logic Theories

10.29007/7gg3 ◽  
2018 ◽  
Author(s):  
Joe Hurd
Keyword(s):  
Theory Development ◽  
Interactive Theorem Proving ◽  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
Domain Specific ◽  
Language Functions ◽  
Hol Light ◽  
Dependency Structures

Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is effective package management, which has the potential to simplify the development of logical theories by precisely checking dependencies and promoting re-use. This paper introduces a domain-specific language for defining composable packages of higher order logic theories, which is designed to naturally handle the complex dependency structures that often arise in theory development. The package composition language functions as a module system for theories, and the paper presents a well-defined semantics for the supported operations. Preliminary tests of the package language and its toolset have been made by packaging the theories distributed with the HOL Light theorem prover. This experience is described, leading to some initial theory engineering discussion on the ideal properties of a reusable theory.

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 Proof-producing translation of higher-order logic into pure and stateful ML

2014 ◽  
Vol 24 (2-3) ◽  
pp. 284-315 ◽  
Author(s):  
MAGNUS O. MYREEN ◽  
SCOTT OWENS
Keyword(s):  
Programming Language ◽  
Operational Semantics ◽  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Theoretic Model ◽  
Logical Function ◽  
Functional Program ◽  
Higher Order Logic ◽  
Hol Light

AbstractThe higher-order logic found in proof assistants such as Coq and various HOL systems provides a convenient setting for the development and verification of functional programs. However, to efficiently run these programs, they must be converted (or ‘extracted’) to functional programs in a programming language such as ML or Haskell. With current techniques, this step, which must be trusted, relates similar looking objects that have very different semantic definitions, such as the set-theoretic model of a logic and the operational semantics of a programming language. In this paper, we show how to increase the trustworthiness of this step with an automated technique. Given a functional program expressed in higher-order logic, our technique provides the corresponding program for a functional language defined with an operational semantics, and it provides a mechanically checked theorem relating the two. This theorem can then be used to transfer verified properties of the logical function to the program. We have implemented our technique in the HOL4 theorem prover, translating functions to a subset of Standard ML, and have applied the implementation to examples including functional data structures, a parser generator, cryptographic algorithms, a garbage collector and the 500-line kernel of the HOL light theorem prover. This paper extends our previous conference publication with new material that shows how functions defined in terms of a state-and-exception monad can be translated, with proofs, into stateful ML code. The HOL light example is also new.

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 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 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.

Sign in / Sign up

Export Citation Format

Share Document