View in EDS

MizAR 40 for Mizar 40.

Saved in:
Bibliographic Details
Title: MizAR 40 for Mizar 40.
Authors: Kaliszyk, Cezary1, Urban, Josef2 Josef.Urban@gmail.com
Source: Journal of Automated Reasoning. Oct2015, Vol. 55 Issue 3, p245-256. 12p.
Subjects: Machine learning, Mathematical proofs, Automation, Real-time control, Computer systems
Abstract: As a present to Mizar on its 40th anniversary, we develop an AI/ATP system that in 30 seconds of real time on a 14-CPU machine automatically proves 40 % of the theorems in the latest official version of the Mizar Mathematical Library ( MML). This is a considerable improvement over previous performance of large-theory AI/ATP methods measured on the whole MML. To achieve that, a large suite of AI/ATP methods is employed and further developed. We implement the most useful methods efficiently, to scale them to the 150000 formulas in MML. This reduces the training times over the corpus to 1-3 seconds, allowing a simple practical deployment of the methods in the online automated reasoning service for the Mizar users ( Miz $\mathbb {A}\mathbb {R}$). [ABSTRACT FROM AUTHOR]
Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 109992872
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: MizAR 40 for Mizar 40.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Kaliszyk%2C+Cezary%22">Kaliszyk, Cezary</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Urban%2C+Josef%22">Urban, Josef</searchLink><relatesTo>2</relatesTo><i> Josef.Urban@gmail.com</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Automated+Reasoning%22">Journal of Automated Reasoning</searchLink>. Oct2015, Vol. 55 Issue 3, p245-256. 12p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Machine+learning%22">Machine learning</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+proofs%22">Mathematical proofs</searchLink><br /><searchLink fieldCode="DE" term="%22Automation%22">Automation</searchLink><br /><searchLink fieldCode="DE" term="%22Real-time+control%22">Real-time control</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+systems%22">Computer systems</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: As a present to Mizar on its 40th anniversary, we develop an AI/ATP system that in 30 seconds of real time on a 14-CPU machine automatically proves 40 % of the theorems in the latest official version of the Mizar Mathematical Library ( MML). This is a considerable improvement over previous performance of large-theory AI/ATP methods measured on the whole MML. To achieve that, a large suite of AI/ATP methods is employed and further developed. We implement the most useful methods efficiently, to scale them to the 150000 formulas in MML. This reduces the training times over the corpus to 1-3 seconds, allowing a simple practical deployment of the methods in the online automated reasoning service for the Mizar users ( Miz $\mathbb {A}\mathbb {R}$). [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=109992872
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10817-015-9330-8
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 12
        StartPage: 245
    Subjects:
      – SubjectFull: Machine learning
        Type: general
      – SubjectFull: Mathematical proofs
        Type: general
      – SubjectFull: Automation
        Type: general
      – SubjectFull: Real-time control
        Type: general
      – SubjectFull: Computer systems
        Type: general
    Titles:
      – TitleFull: MizAR 40 for Mizar 40.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Kaliszyk, Cezary
      – PersonEntity:
          Name:
            NameFull: Urban, Josef
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 10
              Text: Oct2015
              Type: published
              Y: 2015
          Identifiers:
            – Type: issn-print
              Value: 01687433
          Numbering:
            – Type: volume
              Value: 55
            – Type: issue
              Value: 3
          Titles:
            – TitleFull: Journal of Automated Reasoning
              Type: main
ResultId 1