MaLARea SG1 - Machine learner for automated reasoning with semantic guidance

Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jiří Vyskočil

Research output: Chapter in Book/Report/Conference proceedingConference contribution

59 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationAutomated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings
Pages441-456
Number of pages16
DOIs
StatePublished - 2008
Event4th International Joint Conference on Automated Reasoning, IJCAR 2008 - Sydney, NSW, Australia
Duration: Aug 12 2008Aug 15 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5195 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Joint Conference on Automated Reasoning, IJCAR 2008
CountryAustralia
CitySydney, NSW
Period8/12/088/15/08

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'MaLARea SG1 - Machine learner for automated reasoning with semantic guidance'. Together they form a unique fingerprint.

  • Cite this

    Urban, J., Sutcliffe, G., Pudlák, P., & Vyskočil, J. (2008). MaLARea SG1 - Machine learner for automated reasoning with semantic guidance. In Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings (pp. 441-456). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5195 LNAI). https://doi.org/10.1007/978-3-540-71070-7_37