An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic

Understand

Automated theorem proving in first-order logic is an active research area which is successfully supported by machine learning.

• While there have been various proposals for encoding logical formulas into numerical vectors -- from simple strings to more involved graph-based embeddings -- little is known about how these different encodings compare.
• In this paper, we study and experimentally compare pattern-based embeddings that are applied in current systems with popular graph-based encodings, most of which have not been considered in the theorem proving context before.
• Our experiments show that the advantages of simpler encoding schemes in terms of runtime are outdone by more complex graph-based embeddings, which yield more efficient search strategies and simpler proofs.