arXiv Open Access 2019

Domain-Specific Language to Encode Induction Heuristics

Yutaka Nagashima

Lihat Sumber

Abstrak

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 present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics specified by experienced users, thus systematically transferring experienced users' expertise to new Isabelle users.

Topik & Kata Kunci

cs.LO

Penulis (1)

Yutaka Nagashima

Format Sitasi

APA MLA BibTeX

Nagashima, Y. (2019). Domain-Specific Language to Encode Induction Heuristics. https://arxiv.org/abs/1907.02594

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2019
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓