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

1. 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.
2. To reach end users, we will integrate the automatic provers in interactive tools: both general-purpose proof assistants and software verification platforms.

Case Studies

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

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

Community Building

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
• Formalize research in computer science and mathematics

This will lead to more trustworthy software and science.