Machine Learning Guidance for Connection Tableaux

Area of Science:

• Automated reasoning
• Logic and computation

Background:

• Connection calculi provide efficient goal-directed proof search.
• Connection tableaux are a specific type of connection calculus.

Purpose of the Study:

• To present optimized functional implementations of connection tableaux proof search.
• To introduce machine learning-based guidance methods for proof search.

Main Methods:

• Optimized functional implementations of connection tableaux.
• A consistent Skolemisation procedure tailored for machine learning.
• Naive Bayesian probabilities for reordering proof steps.
• Monte Carlo Tree Search for expanding the proof search tree.

Main Results:

• Demonstration of optimized functional implementations for connection tableaux.
• Successful integration of a consistent Skolemisation procedure.
• Effective application of Naive Bayesian probabilities for proof step reordering.
• Efficient proof search tree expansion using Monte Carlo Tree Search.

Conclusions:

• Optimized implementations and machine learning guidance enhance connection tableaux proof search.
• The presented methods offer advancements in automated reasoning and theorem proving.