7 citations · 25 across the 19 of their papers we have counts for
19 papers
Abduction Prover in Isabelle/HOL
Yutaka Nagashima, Daniel Sebastian Goc
Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assistants. We address this problem b…
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
Yutaka Nagashima, Zijin Xu, Ningli Wang +2
Proof by induction plays a central role in formal verification. However, its automation remains as a formidable challenge in Computer Science. To solve inductive problems, human en…
Genetic Algorithm for Program Synthesis
Yutaka Nagashima
A deductive program synthesis tool takes a specification as input and derives a program that satisfies the specification. The drawback of this approach is that search spaces for su…
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
Yutaka Nagashima
Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a bo…
Faster Smarter Induction in Isabelle/HOL
Yutaka Nagashima
Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science…
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Yutaka Nagashima
Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esot…
Towards United Reasoning for Automatic Induction in Isabelle/HOL
Yutaka Nagashima
Inductive theorem proving is an important long-standing challenge in computer science. In this extended abstract, we first summarize the recent developments of proof by induction f…
Smart Induction for Isabelle/HOL (System Description)
Yutaka Nagashima
Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to those induction tactics. To automate t…
Domain-Specific Language to Encode Induction Heuristics
Yutaka Nagashima
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, they did not have a…
Designing Game of Theorems
Yutaka Nagashima
"Theorem proving is similar to the game of Go. So, we can probably improve our provers using deep learning, like DeepMind built the super-human computer Go program, AlphaGo." Such…
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Yutaka Nagashima
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however, there is a little to…
Towards Evolutionary Theorem Proving for Isabelle/HOL
Yutaka Nagashima
Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proof…
Towards Machine Learning Induction
Yutaka Nagashima
Induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first…
Goal-Oriented Conjecturing for Isabelle/HOL
Yutaka Nagashima, Julian Parsert
We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transformin…
PaMpeR: Proof Method Recommendation System for Isabelle/HOL
Yutaka Nagashima, Yilun He
Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system fo…
Towards Smart Proof Search for Isabelle
Yutaka Nagashima
Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this position paper we first report our…
Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML
Yutaka Nagashima, Liam O'Connor
We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses.
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
Yutaka Nagashima, Ramana Kumar
We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines…
COGENT: Certified Compilation for a Functional Systems Language
Liam O'Connor, Christine Rizkallah, Zilin Chen +8
We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and witho…