About: MaLARea SG1 - Machine learner for automated reasoning with semantic guidance     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

AttributesValues
rdf:type
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.
  • 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. (en)
  • Č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. (cs)
Title
  • MaLARea SG1 - Machine learner for automated reasoning with semantic guidance
  • MaLARea SG1 - Machine learner for automated reasoning with semantic guidance (en)
  • MaLARea SG1 - Strojové učení se pro automatické dokazování se sémantickým řízením (cs)
skos:prefLabel
  • MaLARea SG1 - Machine learner for automated reasoning with semantic guidance
  • MaLARea SG1 - Machine learner for automated reasoning with semantic guidance (en)
  • MaLARea SG1 - Strojové učení se pro automatické dokazování se sémantickým řízením (cs)
skos:notation
  • RIV/00216208:11320/08:00100073!RIV09-MSM-11320___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • Z(MSM0021620838)
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 377517
http://linked.open...ai/riv/idVysledku
  • RIV/00216208:11320/08:00100073
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • MaLARea; Machine; learner; automated; reasoning; semantic; guidance (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [2C120C892182]
http://linked.open...v/mistoKonaniAkce
  • HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY
http://linked.open...i/riv/mistoVydani
  • HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY
http://linked.open...i/riv/nazevZdroje
  • Proceedings of the 4th International Joint Conference on Automated Reasoning
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Urban, Josef
  • Vyskočil, Jiří
  • Sutcliffe, Geoff
  • Pudlák, Petr
http://linked.open...vavai/riv/typAkce
http://linked.open...ain/vavai/riv/wos
  • 000258887400037
http://linked.open.../riv/zahajeniAkce
http://linked.open...n/vavai/riv/zamer
number of pages
http://purl.org/ne...btex#hasPublisher
  • SPRINGER-VERLAG BERLIN
https://schema.org/isbn
  • 978-3-540-71069-1
http://localhost/t...ganizacniJednotka
  • 11320
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 48 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software