Zobrazeno 1 - 10
of 57
pro vyhledávání: '"Nagashima, Yutaka"'
Autor:
Nagashima, Yutaka
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 such correct programs tend to be enormous, making it difficult to derive
Externí odkaz:
http://arxiv.org/abs/2211.11937
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 engineers often have to provide auxiliary lemmas manually. We automate t
Externí odkaz:
http://arxiv.org/abs/2212.11151
Autor:
Nagashima, Yutaka
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 boolean query language to represent experienced users' knowledge on how
Externí odkaz:
http://arxiv.org/abs/2010.10296
Autor:
Nagashima, Yutaka
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. To address this problem, we developed sem_ind. Given inductive probl
Externí odkaz:
http://arxiv.org/abs/2009.09215
Autor:
Nagashima, Yutaka
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 for Isabelle/HOL. Then, we propose united reasoning, a novel approach t
Externí odkaz:
http://arxiv.org/abs/2005.12737
Autor:
Nagashima, Yutaka
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 esoteric structures of proof documents impede machine learning practitione
Externí odkaz:
http://arxiv.org/abs/2004.10667
Autor:
Nagashima, Yutaka
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 this process, we present smart_induct for Isabelle/HOL. Given an induct
Externí odkaz:
http://arxiv.org/abs/2001.10834
Autor:
Nagashima, Yutaka
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 systematic way to encode their expertise. To address this problem, we
Externí odkaz:
http://arxiv.org/abs/1907.02594
Autor:
Nagashima, Yutaka
"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 optimism has been observed among participants of AITP2017. But is theo
Externí odkaz:
http://arxiv.org/abs/1906.08549
Autor:
Nagashima, Yutaka
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 tool support for transferring this expert knowledge to a wider user audi
Externí odkaz:
http://arxiv.org/abs/1906.08084