44 citations · 108 across the 12 of their papers we have counts for
Showing 2018Show all
2 papers · 1 filter
cs.AI2018★ 44 cited
TacticToe: Learning to Prove with Tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban +2
We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in eac…
cs.LO2018
Clocked Definitions in HOL
Ramana Kumar, Magnus O. Myreen
Many potentially non-terminating functions cannot be directly defined in a logic of total functions, such as HOL. A well-known solution to this is to define non-terminating functio…