A proof strategy language and proof script generation for Isabelle/HOL

DOI10.1007/978-3-319-63046-5_32zbMath1494.68290arXiv1606.02941OpenAlexW2962820807MaRDI QIDQ2405272

Ramana Kumar, Yutaka Nagashima

Publication date: 22 September 2017

Full work available at URL: https://arxiv.org/abs/1606.02941

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Online machine learning techniques for Coq: a comparison ⋮ TacticToe: learning to prove with tactics

Uses Software

• Coq
• Isabelle/HOL
• IsaPlanner
• PVS
• Sledgehammer
• Lean
• SEPIA

This page was built for publication: A proof strategy language and proof script generation for Isabelle/HOL