Back to Search
Start Over
Neural Precedence Recommender
- Source :
- Automated Deduction – CADE 28 ISBN: 9783030798758, CADE
- Publication Year :
- 2021
- Publisher :
- Springer International Publishing, 2021.
-
Abstract
- The state-of-the-art superposition-based theorem provers for first-order logic rely on simplification orderings on terms to constrain the applicability of inference rules, which in turn shapes the ensuing search space. The popular Knuth-Bendix simplification ordering is parameterized by symbol precedence—a permutation of the predicate and function symbols of the input problem’s signature. Thus, the choice of precedence has an indirect yet often substantial impact on the amount of work required to complete a proof search successfully.This paper describes and evaluates a symbol precedence recommender, a machine learning system that estimates the best possible precedence based on observations of prover performance on a set of problems and random precedences. Using the graph convolutional neural network technology, the system does not presuppose the problems to be related or share a common signature. When coupled with the theorem prover Vampire and evaluated on the TPTP problem library, the recommender is found to outperform a state-of-the-art heuristic by more than 4 % on unseen problems.
- Subjects :
- Theoretical computer science
Computer science
Parameterized complexity
020207 software engineering
0102 computer and information sciences
02 engineering and technology
Predicate (mathematical logic)
Function (mathematics)
01 natural sciences
Signature (logic)
Permutation
Superposition principle
010201 computation theory & mathematics
0202 electrical engineering, electronic engineering, information engineering
Rule of inference
Symbol (formal)
Subjects
Details
- ISBN :
- 978-3-030-79875-8
- ISBNs :
- 9783030798758
- Database :
- OpenAIRE
- Journal :
- Automated Deduction – CADE 28 ISBN: 9783030798758, CADE
- Accession number :
- edsair.doi...........fbd3df1686fa5812986fa74596cf1180