Realizing the Promise of Higher-Order SMT and Superposition for Interactive Verification

Introduction

Proof assistants (also called interactive theorem provers) have a long history of being very tedious to use. The situation has improved markedly in the past decade with the integration of first-order automatic theorem provers as backends.

Recent Developments

Recently, there have been exciting developments for more expressive logics, with the emergence of automatic provers based on optimized higher-order calculi.

Project Aim

The Nekoka project's aim is to make higher-order SMT and λ-superposition a perfect fit for logical problems emerging from the verification of software and mathematics.

Implementation Strategy

We will start by extending higher-order SMT and λ-superposition and implementing them in automatic provers to provide push-button proof automation for lemmas expressed in higher-order logics.

Integration with Tools

To reach end users, we will integrate the automatic provers in interactive tools:

• General-purpose proof assistants
• Software verification platforms

Case Studies

As case studies, we will use our own provers and integrations to:

1. Formalize quantum information theory
2. Verify a big data framework in collaboration with domain experts

Beyond providing representative case studies, this will help build a user community around our tools and technologies.

Scientific Impact

In terms of scientific impact, the improved higher-order SMT and λ-superposition calculi will substantially advance the art of higher-order automation and help reorient research in automated reasoning towards the needs of end users, whether computer scientists or mathematicians.

Long-term Vision

Our tools will outlive the project, serving end users and continuing to be useful for future research.

Societal Impact

At the societal level, the project will herald a future in which automatic provers and proof assistants are routinely deployed in tandem to verify critical computing infrastructure and to formalize research in computer science and mathematics, thereby leading to more trustworthy software and science.