
SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL
Proof assistants offer tactics to apply proof by induction, but these ta...
read it

Faster Smarter Induction in Isabelle/HOL
We present semantic_induct, an automatic tool to recommend how to apply ...
read it

Towards United Reasoning for Automatic Induction in Isabelle/HOL
Inductive theorem proving is an important longstanding challenge in com...
read it

Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Recently, a growing number of researchers have applied machine learning ...
read it

Smart Induction for Isabelle/HOL (System Description)
Proof assistants offer tactics to facilitate inductive proofs. However, ...
read it

DomainSpecific Language to Encode Induction Heuristics
Proof assistants, such as Isabelle/HOL, offer tools to facilitate induct...
read it

Designing Game of Theorems
"Theorem proving is similar to the game of Go. So, we can probably impro...
read it

LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Proof assistants, such as Isabelle/HOL, offer tools to facilitate induct...
read it

Towards Evolutionary Theorem Proving for Isabelle/HOL
Mechanized theorem proving is becoming the basis of reliable systems pro...
read it

Towards Machine Learning Induction
Induction lies at the heart of mathematics and computer science. However...
read it

Towards Machine Learning Mathematical Induction
Mathematical induction lies at the heart of mathematics and computer sci...
read it

PaMpeR: Proof Method Recommendation System for Isabelle/HOL
Deciding which subtool to use for a given proof state requires expertis...
read it

GoalOriented Conjecturing for Isabelle/HOL
We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof...
read it

Towards Smart Proof Search for Isabelle
Despite the recent progress in automatic theorem provers, proof engineer...
read it
Yutaka Nagashima
is this you? claim profile