Proof General中的机器学习：接口的接口
人工智能
2013-07-09 v2 机器学习
计算机科学中的逻辑
摘要
我们介绍了ML4PG——Proof General的机器学习扩展。它允许用户从Coq和SSReflect编写的交互式高阶证明库中收集与目标形状、应用策略序列和证明树结构相关的证明统计信息。使用MATLAB和Weka中最先进的机器学习算法对收集的数据进行聚类。ML4PG提供了Proof General与MATLAB/Weka之间的自动接口。聚类结果被ML4PG用于在交互式证明开发过程中提供证明提示。
引用
@article{arxiv.1212.3618,
title = {Machine Learning in Proof General: Interfacing Interfaces},
author = {Ekaterina Komendantskaya and Jónathan Heras and Gudmund Grov},
journal= {arXiv preprint arXiv:1212.3618},
year = {2013}
}
备注
In Proceedings UITP 2012, arXiv:1307.1528