Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants

We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. From this point of view, it seems desirable to enrich superposition and SMT (satisfiability modulo theories) with higher-order reasoning in a careful manner, to preserve their good properties. Representative benchmarks from the interactive community can guide the design of proof rules and strategies. With higher-order superposition and higher-order SMT in place, highly automatic provers could be built on modern superposition provers and SMT solvers, following a stratified architecture reminiscent of that of modern SMT solvers. We hope that these provers will bring a new level of automation to the users of proof assistants. These challenges and work plan are at the core of the Matryoshka project, funded for five years by the European Research Council. We encourage researchers motivated by the same goals to get in touch with us, subscribe to our mailing list, and join forces.

Download Full-text

Interactive proof-search for equational reasoning

Logic Journal of IGPL ◽

10.1093/jigpal/jzaa013 ◽

2020 ◽

Author(s):

Favio E Miranda-Perea ◽

Lourdes del Carmen González Huesca ◽

P Selene Linares-Arévalo

Keyword(s):

Functional Programming ◽

Formal System ◽

Deductive System ◽

Proof Assistants ◽

Interactive Proof ◽

Equational Reasoning ◽

Mathematical Proofs ◽

Proof Search ◽

The Common ◽

Definition Of

Abstract Equational reasoning arises in many areas of mathematics and computer science. It is a cornerstone of algebraic reasoning and results essential in tasks of specification and verification in functional programming, where a program is mainly a set of equations. The usual manipulation of identities while conducting informal proofs obviates many intermediate steps that are neccesary while developing them using a formal system, such as the equationally complete Birkhoff calculus ${\mathcal{B}}$. This deductive system does not fit in the common manner of doing mathematical proofs, and it is not compatible with the mechanisms of proof assistants. The aim of this work is to provide a deductive system ${\mathcal{B}}^{\textrm{GOAL}}$ for equality, equivalent to ${\mathcal{B}}$ but suitable for constructing equational proofs in a backward fashion. This feature makes it adequate for interactive proof-search in the approach of proof assistants. This will be achieved by turning ${\mathcal{B}}^{\textrm{GOAL}}$ into a transition system of formal tactics in the style of Edinburgh LCF, such transformation allows us to give a direct formal definition of backward proof in equational logic.

Download Full-text

Going Polymorphic - TH1 Reasoning for Leo-III

10.29007/jgkw ◽

2018 ◽

Cited By ~ 1

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.

Download Full-text

Secure Cloud Quantum Computing with Verification Based on Quantum Interactive Proof

Impact ◽

10.21820/23987073.2019.10.30 ◽

2019 ◽

Vol 2019 (10) ◽

pp. 30-32

Author(s):

Tomoyuki Morimae

Keyword(s):

Quantum Computing ◽

Quantum Information ◽

Theoretical Physics ◽

View Point ◽

Research Subjects ◽

Interactive Proof ◽

Open Problems ◽

Main Research ◽

Proof Systems ◽

Information Group

In cloud quantum computing, a classical client delegate quantum computing to a remote quantum server. An important property of cloud quantum computing is the verifiability: the client can check the integrity of the server. Whether such a classical verification of quantum computing is possible or not is one of the most important open problems in quantum computing. We tackle this problem from the view point of quantum interactive proof systems. Dr Tomoyuki Morimae is part of the Quantum Information Group at the Yukawa Institute for Theoretical Physics at Kyoto University, Japan. He leads a team which is concerned with two main research subjects: quantum supremacy and the verification of quantum computing.

Download Full-text