Sciweavers

Share
CADE
2008
Springer

MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance

9 years 2 months ago
MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance
This paper describes a system combining model-based and learning-based methods for automated reasoning in large theories, i.e. on a large number of problems that use many axioms, lemmas, theorems, definitions, and symbols, in a consistent fashion. The implementation is based on the existing MaLARea system, which cycles between theorem proving attempts and learning axiom relevance from successes. This system is extended by taking into account semantic relevance of axioms, in a way similar to that of the SRASS system. The resulting combined system significantly outperforms both MaLARea and SRASS on the MPTP Challenge large theory benchmark, in terms of both the number of problems solved and the time taken to find solutions. The design, implementation, and experimental testing of the system are described here.
Geoff Sutcliffe, Jirí Vyskocil, Josef Urban
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Geoff Sutcliffe, Jirí Vyskocil, Josef Urban, Petr Pudlák
Comments (0)
books