MaLARea SG1 - Machine learner for automated reasoning with semantic guidance

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

MaLARea SG1 - Machine learner for automated reasoning with semantic guidance

Original language description

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.

Czech name

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

Czech description

Článek popisuje v současnosti nejsilnejší existující systém pro automatické dokazování vět nad velkými matematickými teoriemi jako je databáze Mizar. Systém propojuje sémantické metody založené na tvorbě a použití databáze modelů s metodami strojového učení z předchozích důkazů, a používá tyto metody pro výběr dostatečně malé množiny nejrelevantnejších axiomů vhodných pro důkaz hypotéz. Tento systém zvítězil v kategorii řešení velkých matematických problémů (MZR) letošního (2008) ročníku soutěže automatických dokazovačů (CASC) v Sydney, a vyřešil 1.5-krát více problémů než druhý nejlepší systém v této kategorii.

Type

D - Article in proceedings

CEP classification

JD - Use of computers, robotics and its application

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2008

Confidentiality

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

Article name in the collection

Proceedings of the 4th International Joint Conference on Automated Reasoning

ISBN

978-3-540-71069-1

ISSN

—

e-ISSN

—

Number of pages

16

Pages from-to

—

Publisher name

SPRINGER-VERLAG BERLIN

Place of publication

HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY

Event location

HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY

Event date

Jan 1, 2008

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000258887400037