TacticToe: learning to prove with tactics
type: Item
instance of: scholarly article
title: TacticToe: learning to prove with tactics
author: T. Gauthier
author: Cezary Kaliszyk
author: Josef Urban
author: Ramana Kumar
author: Michael Norrish
published in: Journal of Automated Reasoning
publication date: 2021-06-09T00:00:00Z
full work available at URL: https://arxiv.org/abs/1804.00596
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7356973
zbMATH Keywords: machine learning
zbMATH Keywords: tactic
zbMATH Keywords: policy
zbMATH Keywords: interactive theorem prover
zbMATH Keywords: HOL4
zbMATH Keywords: tree search
zbMATH Keywords: theorem
zbMATH Keywords: formalization
describes a project that uses: HOL
describes a project that uses: Coq
describes a project that uses: MPTP
describes a project that uses: Tactician
describes a project that uses: CLAM
describes a project that uses: Oyster
describes a project that uses: SEPIA
describes a project that uses: TacticToe
describes a project that uses: IsaPlanner
describes a project that uses: Metis_
describes a project that uses: Isabelle
describes a project that uses: E Theorem Prover
describes a project that uses: Eisbach
describes a project that uses: OpenTheory
describes a project that uses: HOL Light
describes a project that uses: ML4PG
describes a project that uses: MaLeCoP
describes a project that uses: Flyspeck
describes a project that uses: MaLARea
describes a project that uses: FEMaLeCoP
MaRDI profile type: Publication
OpenAlex ID: W3080426653
Wikidata QID: Q108482100
cites work: Refactoring Proofs with Tactician
cites work: Ωmega: Towards a mathematical assistant
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Hammering towards QED
cites work: A learning-based fact selector for Isabelle/HOL
cites work: Reducing higher-order theorem proving to a sequence of SAT problems
cites work: Q3804239
cites work: Q2767010
cites work: Internal Guidance for Satallax
cites work: TacticToe: Learning to Reason with HOL4 Tactics
cites work: SEPIA: Search for Proofs Using Inferred Automata
cites work: HOL Light: An Overview
cites work: Recycling proof patterns in Coq: case studies
cites work: Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
cites work: FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
cites work: MizAR 40 for Mizar 40
cites work: Standalone Tactics Using OpenTheory
cites work: Eisbach: a proof method language for Isabelle
cites work: Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
cites work: A proof strategy language and proof script generation for Isabelle/HOL
cites work: Q3150301
cites work: A Brief Overview of HOL4
cites work: MPTP-motivation, implementation, first experiments
cites work: ATP and presentation service for Mizar formalizations
cites work: MaLeCoP Machine Learning Connection Prover
cites work: The Isabelle Framework
cites work: Q3024890
cites work: The OYSTER-CLAM system
DOI: 10.1007/S10817-020-09580-X
description: scientific article; zbMATH DE number 7356973