Machine Learning Guidance and Proof Certification for Connection Tableaux

Michael Färber, Cezary Kaliszyk, Josef Urban

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 opti…