Monte Carlo Tree Search (MCTS) is a technique to guide search in a large decision space by taking random samples and evaluating their outcome. In this work, we study MCTS methods in the context of the connection calculus and implement them on top of the leanCoP prover. This includes proposing useful proof-state evaluation heuristics that are learned from previous proofs, and proposing and automatically improving suitable MCTS strategies in this context. The system is trained and evaluated on a large suite of related problems coming from the Mizar proof assistant, showing that it is capable to find new and different proofs. To our knowledge, this is the first time MCTS has been applied to theorem proving.
This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.
A THEOREM-PROVER FOR A DECIDABLE SUBSET OF DEFAULT LOGIC Philippe BESNARD - Rene QUINIOU - Patrice QUINTON IRISA - INRIA Rennes Campus de Beaulieu 35042 RENNES Cedex FRANCE Abstract II DEFAULT LOGIC Nonmonotonic logic is an attempt to take into account such notions as incomplete knowledge and theory evolution. However the decidable theorem-prover issue has been so far unexplored. We propose such a theorem-prover for default logic with a restriction on the first-order formulae it deals with. This theorem-prover is based on the generalisation of a resolution technique named saturation, which was initially designed to test the consistency of a set of first-order formulae. We have proved that our algorithm is complete and that it always terminates for the selected subset of first-order formulae.
A near-propositional CNF formula is a first-order formula (in clause normal form) with a finite Herbrand universe. For this class of problems, the validity problem can be decided by a combination of grounding and propositional reasoning. However, naive approaches to grounding can generate extremely large ground formulae. We investigate various means to reduce the number of ground instances generated and show that we can increase the number of problems that can be handled with reasonable resources.