Tactic Learning and Proving for the Coq Proof Assistant

20 March 2020

Papers citing "Tactic Learning and Proving for the Coq Proof Assistant"

5 / 5 papers shown

Title
Proof Recommendation System for the HOL4 Theorem Prover Nour Dekhil Adnan Rashid Sofiene Tahar 48 1 0 31 Dec 2024
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning Minchao Wu Michael Norrish Christian J. Walder Amir Dezfouli 12 40 0 19 Feb 2021
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction Yutaka Nagashima LRM 16 3 0 19 Oct 2020
Faster Smarter Induction in Isabelle/HOL Yutaka Nagashima 13 7 0 19 Sep 2020
MizAR 40 for Mizar 40 C. Kaliszyk Josef Urban VLM AI4CE LRM AIMat 56 132 0 10 Oct 2013