Mtac: A monad for typed tactic programming in Coq

2015 ◽  
Vol 25 ◽  
Author(s):  
BETA ZILIANI ◽  
DEREK DREYER ◽  
NEELAKANTAN R. KRISHNASWAMI ◽  
ALEKSANDAR NANEVSKI ◽  
VIKTOR VAFEIADIS
Keyword(s):  
Large Scale ◽  
Type Inference ◽  
Theorem Prover ◽  
Interactive Proof ◽  
Theorem Provers ◽  
Proof Automation ◽  
Base Logic

AbstractEffective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers.We present Mtac, a lightweight but powerful extension to Coq that supports dependently typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.

scholarly journals How to make ad hoc proof automation less ad hoc

2013 ◽  
Vol 23 (4) ◽  
pp. 357-401 ◽  
Author(s):  
GEORGES GONTHIER ◽  
BETA ZILIANI ◽  
ALEKSANDAR NANEVSKI ◽  
DEREK DREYER
Keyword(s):  
Design Patterns ◽  
Ad Hoc ◽  
Type System ◽  
Type Inference ◽  
Interactive Theorem Provers ◽  
Proof Automation ◽  
Novel Approach ◽  
Type Classes ◽  
Structure Programming ◽  
Base Logic

AbstractMost interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.

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.

CALL FOR PAPERS Journal of Functional Programming Special Issue on Theorem Provers and Functional Programming

1997 ◽  
Vol 7 (1) ◽  
pp. 125-126
Author(s):  
Tom Melham
Keyword(s):  
Interface Design ◽  
Functional Programming ◽  
Type Systems ◽  
Theory And Practice ◽  
Theorem Prover ◽  
Functional Languages ◽  
Special Issue ◽  
Theorem Provers ◽  
Problems And Solutions ◽  
Submission Deadline

A special issue of the Journal of Functional Programming will be devoted to the use of functional programming in theorem proving. The submission deadline is 31 August 1997.The histories of theorem provers and functional languages have been deeply intertwined since the advent of Lisp. A notable example is the ML family of languages, which are named for the meta language devised for the LCF theorem prover, and which provide both the implementation platform and interaction facilities for numerous later systems (such as Coq, HOL, Isabelle, NuPrl). Other examples include Lisp (as used for ACL2, PVS, Nqthm) and Haskell (as used for Veritas).This special issue is devoted to the theory and practice of using functional languages to implement theorem provers and using theorem provers to reason about functional languages. Topics of interest include, but are not limited to:– architecture of theorem prover implementations– interface design in the functional context– limits of the LCF methodology– impact of host language features– type systems– lazy vs strict languages– imperative (impure) features– performance problems and solutions– problems of scale– special implementation techniques– term representations (e.g. de Bruijn vs name carrying vs BDDs)– limitations of current functional languages– mechanised theories of functional programming

scholarly journals Breeding Theorem Proving Heuristics with Genetic Algorithms

10.29007/gms9 ◽  
2018 ◽  
Author(s):  
Simon Schäfer ◽  
Stephan Schulz
Keyword(s):  
Genetic Algorithms ◽  
Large Scale ◽  
First Order ◽  
Proof Search ◽  
Theorem Provers ◽  
Search Heuristics ◽  
Practical Performance ◽  
Set Up ◽  
The Given ◽  
Selection Of

First-order theorem provers have to search for proofs in an infinitespace of possible derivations. Proof search heuristics play a vitalrole for the practical performance of these systems. In the currentgeneration of saturation-based theorem provers like SPASS, E,Vampire or Prover~9, one of the most important decisions is theselection of the next clause to process with the given clausealgorithms. Provers offer a wide variety of basic clause evaluationfunctions, which can often be parameterized and combined in manydifferent ways. Finding good strategies is usually left to the usersor developers, often backed by large-scale experimentalevaluations. We describe a way to automatize this process usinggenetic algorithms, evaluating a population of different strategieson a test set, and applying mutation and crossover operators to goodstrategies to create the next generation. We describe the design andexperimental set-up, and report on first promising results.

scholarly journals CoCEC: An Automatic Combinational Circuit Equivalence Checker Based on the Interactive Theorem Prover

Complexity ◽  
2021 ◽  
Vol 2021 ◽  
pp. 1-12
Author(s):  
Wilayat Khan ◽  
Farrukh Aslam Khan ◽  
Abdelouahid Derhab ◽  
Adi Alhudhaif
Keyword(s):  
Boolean Functions ◽  
Digital Logic ◽  
Theorem Prover ◽  
Combinational Circuit ◽  
Interactive Proof ◽  
Interactive Theorem Provers ◽  
Hardware Description ◽  
Description Languages ◽  
User Friendly ◽  
Machine Readable

Checking the equivalence of two Boolean functions, or combinational circuits modeled as Boolean functions, is often desired when reliable and correct hardware components are required. The most common approaches to equivalence checking are based on simulation and model checking, which are constrained due to the popular memory and state explosion problems. Furthermore, such tools are often not user-friendly, thereby making it tedious to check the equivalence of large formulas or circuits. An alternative is to use mathematical tools, called interactive theorem provers, to prove the equivalence of two circuits; however, this requires human effort and expertise to write multiple output functions and carry out interactive proof of their equivalence. In this paper, we (1) define two simple, one formal and the other informal, gate-level hardware description languages, (2) design and develop a formal automatic combinational circuit equivalence checker (CoCEC) tool, and (3) test and evaluate our tool. The tool CoCEC is based on human-assisted theorem prover Coq, yet it checks the equivalence of circuit descriptions purely automatically through a human-friendly user interface. It either returns a machine-readable proof (term) of circuits’ equivalence or a counterexample of their inequality. The interface enables users to enter or load two circuit descriptions written in an easy and natural style. It automatically proves, in few seconds, the equivalence of circuits with as many as 45 variables (3.5   ×   10 13 states). CoCEC has a mathematical foundation, and it is reliable, quick, and easy to use. The tool is intended to be used by digital logic circuit designers, logicians, students, and faculty during the digital logic design course.

scholarly journals Improving ENIGMA-style Clause Selection while Learning From History

2021 ◽  
pp. 543-561
Author(s):  
Martin Suda
Keyword(s):  
Neural Network ◽  
Real Time ◽  
Theorem Prover ◽  
Central Idea ◽  
Theorem Provers ◽  
Recursive Neural Network ◽  
Time Evaluation ◽  
Automatic Theorem ◽  
Learning From History

AbstractWe re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recognizing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We propose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a recursive neural network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The automatic theorem prover Vampire guided by the network achieves a 41 % improvement on a relevant subset of SMT-LIB in a real time evaluation.

Chapter 12. Learning Reasoning Strategies in End-to-End Differentiable Proving

2021 ◽  
Author(s):  
Pasquale Minervini ◽  
Sebastian Riedel ◽  
Pontus Stenetorp ◽  
Edward Grefenstette ◽  
Tim Rocktäschel
Keyword(s):  
Large Scale ◽  
Source Code ◽  
Back Propagation ◽  
Selection Strategy ◽  
Rule Based ◽  
Reasoning Strategies ◽  
Theorem Provers ◽  
Gradient Based ◽  
Learning To Reason ◽  
Yield State

Attempts to render deep learning models interpretable, data-efficient, and robust have seen some success through hybridisation with rule-based systems, for example, in Neural Theorem Provers (NTPs). These neuro-symbolic models can induce interpretable rules and learn representations from data via back-propagation, while providing logical explanations for their predictions. However, they are restricted by their computational complexity, as they need to consider all possible proof paths for explaining a goal, thus rendering them unfit for large-scale applications. We present Conditional Theorem Provers (CTPs), an extension to NTPs that learns an optimal rule selection strategy via gradient-based optimisation. We show that CTPs are scalable and yield state-of-the-art results on the CLUTRR dataset, which tests systematic generalisation of neural models by learning to reason over smaller graphs and evaluating on larger ones. Finally, CTPs show better link prediction results on standard benchmarks in comparison with other neural-symbolic models, while being explainable. All source code and datasets are available online. (At https://github.com/uclnlp/ctp)

STRATEGY PARALLELISM IN AUTOMATED THEOREM PROVING

1999 ◽  
Vol 13 (02) ◽  
pp. 219-245 ◽  
Author(s):  
ANDREAS WOLF ◽  
REINHOLD LETZ
Keyword(s):  
Theorem Proving ◽  
Experimental Evaluation ◽  
Automated Theorem Proving ◽  
Search Strategies ◽  
Theorem Prover ◽  
Strategy Selection ◽  
Theorem Provers ◽  
Initial Strategy ◽  
Basic Concepts ◽  
Run Time

Automated theorem provers use search strategies. Unfortunately, there is no unique strategy which is uniformly successful on all problems. This motivates us to apply different strategies in parallel, in a competitive manner. In this paper, we discuss properties, problems, and perspectives of strategy parallelism in theorem proving. We develop basic concepts like the complementarity and the overlap value of strategy sets. Some of the problems such as initial strategy selection and run-time strategy exchange are discussed in more detail. The paper also contains the description of an implementation of a strategy parallel theorem prover (p-SETHEO) and an experimental evaluation.

scholarly journals Integer Induction in Saturation

2021 ◽  
pp. 361-377
Author(s):  
Petra Hozzová ◽  
Laura Kovács ◽  
Andrei Voronkov
Keyword(s):  
Theorem Proving ◽  
Program Analysis ◽  
State Of The Art ◽  
Inductive Reasoning ◽  
Theorem Prover ◽  
Inference Rules ◽  
First Order ◽  
Theorem Provers ◽  
Mathematical Properties

AbstractIntegers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the theorem prover Vampire and evaluated our work against other state-of-the-art theorem provers. Our results demonstrate the strength of our approach by solving new problems coming from program analysis and mathematical properties of integers.

Sign in / Sign up

Export Citation Format

Share Document