MaLARea SG1 - Machine learner for automated reasoning with semantic guidance

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

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

55 Citations (Scopus)

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 publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages441-456
Number of pages16
Volume5195 LNAI
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Theorem proving
Automated Reasoning
Guidance
Semantics
Testing
Axioms
Cycle System
Theorem Proving
Axiom
Lemma
Model-based
Benchmark
Theorem

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Urban, J., Sutcliffe, G., Pudlák, P., & Vyskočil, J. (2008). MaLARea SG1 - Machine learner for automated reasoning with semantic guidance. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, 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

MaLARea SG1 - Machine learner for automated reasoning with semantic guidance. / Urban, Josef; Sutcliffe, Geoffrey; Pudlák, Petr; Vyskočil, Jiří.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5195 LNAI 2008. p. 441-456 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5195 LNAI).

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

Urban, J, Sutcliffe, G, Pudlák, P & Vyskočil, J 2008, MaLARea SG1 - Machine learner for automated reasoning with semantic guidance. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5195 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5195 LNAI, pp. 441-456, 4th International Joint Conference on Automated Reasoning, IJCAR 2008, Sydney, NSW, Australia, 8/12/08. https://doi.org/10.1007/978-3-540-71070-7_37
Urban J, Sutcliffe G, Pudlák P, Vyskočil J. MaLARea SG1 - Machine learner for automated reasoning with semantic guidance. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5195 LNAI. 2008. p. 441-456. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-71070-7_37
Urban, Josef ; Sutcliffe, Geoffrey ; Pudlák, Petr ; Vyskočil, Jiří. / MaLARea SG1 - Machine learner for automated reasoning with semantic guidance. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5195 LNAI 2008. pp. 441-456 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{976977eb218b4d8ab6164afcf8577416,
title = "MaLARea SG1 - Machine learner for automated reasoning with semantic guidance",
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.",
author = "Josef Urban and Geoffrey Sutcliffe and Petr Pudl{\'a}k and Jiř{\'i} Vyskočil",
year = "2008",
doi = "10.1007/978-3-540-71070-7_37",
language = "English (US)",
isbn = "3540710698",
volume = "5195 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "441--456",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - MaLARea SG1 - Machine learner for automated reasoning with semantic guidance

AU - Urban, Josef

AU - Sutcliffe, Geoffrey

AU - Pudlák, Petr

AU - Vyskočil, Jiří

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=53049092451&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=53049092451&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-71070-7_37

DO - 10.1007/978-3-540-71070-7_37

M3 - Conference contribution

SN - 3540710698

SN - 9783540710691

VL - 5195 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 441

EP - 456

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -