7 citations · 25 across the 19 of their papers we have counts for
10 papers · 1 filter
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…
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…
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…
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…
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…