research
∙
11/22/2022
Genetic Algorithm for Program Synthesis
A deductive program synthesis tool takes a specification as input and de...
share
research
∙
11/20/2022
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
Proof by induction plays a central role in formal verification. However,...
research
∙
10/19/2020
SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL
Proof assistants offer tactics to apply proof by induction, but these ta...
research
∙
09/19/2020
Faster Smarter Induction in Isabelle/HOL
We present semantic_induct, an automatic tool to recommend how to apply ...
research
∙
05/25/2020
Towards United Reasoning for Automatic Induction in Isabelle/HOL
Inductive theorem proving is an important long-standing challenge in com...
research
∙
04/21/2020
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Recently, a growing number of researchers have applied machine learning ...
research
∙
01/27/2020
Smart Induction for Isabelle/HOL (System Description)
Proof assistants offer tactics to facilitate inductive proofs. However, ...
research
∙
06/29/2019
Domain-Specific Language to Encode Induction Heuristics
Proof assistants, such as Isabelle/HOL, offer tools to facilitate induct...
research
∙
06/20/2019
Designing Game of Theorems
"Theorem proving is similar to the game of Go. So, we can probably impro...
research
∙
06/19/2019
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Proof assistants, such as Isabelle/HOL, offer tools to facilitate induct...
research
∙
04/17/2019
Towards Evolutionary Theorem Proving for Isabelle/HOL
Mechanized theorem proving is becoming the basis of reliable systems pro...
research
∙
12/04/2018
Towards Machine Learning Induction
Induction lies at the heart of mathematics and computer science. However...
research
∙
12/04/2018
Towards Machine Learning Mathematical Induction
Mathematical induction lies at the heart of mathematics and computer sci...
research
∙
06/19/2018
PaMpeR: Proof Method Recommendation System for Isabelle/HOL
Deciding which sub-tool to use for a given proof state requires expertis...
research
∙
06/12/2018
Goal-Oriented Conjecturing for Isabelle/HOL
We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof...
research
∙
01/10/2017