TacticToe: learning to prove with tactics

DOI10.1007/s10817-020-09580-xOpenAlexW3080426653WikidataQ108482100 ScholiaQ108482100MaRDI QIDQ2031416

Cezary Kaliszyk, Michael Norrish, Josef Urban, Thibault Gauthier, Ramana Kumar

Publication date: 9 June 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

policymachine learningtree searchformalizationHOL4theoremtacticinteractive theorem prover

Mathematics Subject Classification ID

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

Related Items

Online machine learning techniques for Coq: a comparison, Learning to solve geometric construction problems from images, \textsf{lazyCoP}: lazy paramodulation meets neurally guided search, The role of entropy in guiding a connection prover, CoProver: a recommender system for proof construction, GRUNGE: a grand unified ATP challenge, Guiding an automated theorem prover with neural rewriting

Uses Software

• Coq
• Isabelle
• IsaPlanner
• MPTP
• Metis_
• HOL
• HOL Light
• ML4PG
• MaLeCoP
• E Theorem Prover
• Flyspeck
• MaLARea
• Eisbach
• Tactician
• CLAM
• Oyster
• FEMaLeCoP
• SEPIA
• TacticToe
• OpenTheory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MizAR 40 for Mizar 40
• Eisbach: a proof method language for Isabelle
• A learning-based fact selector for Isabelle/HOL
• Recycling proof patterns in Coq: case studies
• MPTP-motivation, implementation, first experiments
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
• ATP and presentation service for Mizar formalizations
• Reducing higher-order theorem proving to a sequence of SAT problems
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• A proof strategy language and proof script generation for Isabelle/HOL
• Internal Guidance for Satallax
• Standalone Tactics Using OpenTheory
• MaLeCoP Machine Learning Connection Prover
• HOL Light: An Overview
• SEPIA: Search for Proofs Using Inferred Automata
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• A Brief Overview of HOL4
• The Isabelle Framework
• TacticToe: Learning to Reason with HOL4 Tactics
• Refactoring Proofs with Tactician
• Hammering towards QED
• Ωmega: Towards a mathematical assistant