Machine Learning Guidance and Proof Certification for Connection Tableaux

05/08/2018
by   Michael Färber, et al.
0

Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: First, we show optimised functional implementations of clausal and nonclausal proof search, including a consistent Skolemisation procedure for machine learning. Then, we show two guidance methods based on machine learning, namely reordering of proof steps with Naive Bayesian probablities, and expansion of a proof search tree with Monte Carlo Tree Search. Finally, we give a translation of connection proofs to LK, enabling proof certification and automatic proof search in interactive theorem provers.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset