TacticToe: Learning to Reason with HOL4 Tactics

DOI10.29007/ntlbzbMath1403.68224arXiv1804.00595OpenAlexW3105002484WikidataQ108482135 ScholiaQ108482135MaRDI QIDQ4645730

Thibault Gauthier, Cezary Kaliszyk, Josef Urban

Publication date: 10 January 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

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

zbMATH Keywords

automated reasoninghigher-order logicmachine learningproof automationA** proof search

Mathematics Subject Classification ID

Related Items (10)

Online machine learning techniques for Coq: a comparison ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ The role of entropy in guiding a connection prover ⋮ Learning theorem proving components ⋮ Machine Learning for Inductive Theorem Proving ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ TacticToe: learning to prove with tactics ⋮ Towards the automatic mathematician ⋮ GRUNGE: a grand unified ATP challenge ⋮ TacticToe

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• MPTP
• Mizar
• Proof General
• HOL
• HOL Light
• Satallax
• MaLeCoP
• E Theorem Prover
• Flyspeck
• MaLARea

This page was built for publication: TacticToe: Learning to Reason with HOL4 Tactics