Showing cs.LOShow all
3 papers · 1 filter
cs.LO2024
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
Liao Zhang, David M. Cerna, Cezary Kaliszyk
Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theor…
cs.LO2024
Automated Strategy Invention for Confluence of Term Rewrite Systems
Liao Zhang, Fabian Mitterwallner, Jan Jakubuv +1
Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system propertie…
cs.LO2021
Online Machine Learning Techniques for Coq: A Comparison
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski +3
We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin f…