MaLARea SG1 - Strojové učení se pro automatické dokazování se sémantickým řízením

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F08%3A00100073" target="_blank" >RIV/00216208:11320/08:00100073 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

MaLARea SG1 - Machine learner for automated reasoning with semantic guidance

Popis výsledku v původním jazyce

This paper describes a system combining model-based and learning-based methods for automated reasoning in large theories, i.e. oil a large number of problems that use many axioms, lemmas, theorems, definitions, and symbols, in a consistent fashion. The implementation is based oil 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.

Název v anglickém jazyce

MaLARea SG1 - Machine learner for automated reasoning with semantic guidance

Popis výsledku anglicky

This paper describes a system combining model-based and learning-based methods for automated reasoning in large theories, i.e. oil a large number of problems that use many axioms, lemmas, theorems, definitions, and symbols, in a consistent fashion. The implementation is based oil 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.

Druh

D - Stať ve sborníku

CEP obor

JD - Využití počítačů, robotika a její aplikace

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2008

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 4th International Joint Conference on Automated Reasoning

ISBN

978-3-540-71069-1

ISSN

—

e-ISSN

—

Počet stran výsledku

16

Strana od-do

—

Název nakladatele

SPRINGER-VERLAG BERLIN

Místo vydání

HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY

Místo konání akce

HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY

Datum konání akce

1. 1. 2008

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000258887400037