ATP and presentation service for Mizar formalizations

Josef Urban, Piotr Rudnicki, Geoffrey Sutcliffe

Research output: Contribution to journalArticle

34 Citations (Scopus)

Abstract

This paper describes the Automated Reasoning for Mizar (MizAℝ) service, which integrates several automated reasoning, artificial intelligence, and presentation tools with Mizar and its authoring environment. The service provides ATP assistance to Mizar authors in finding and explaining proofs, and offers generation of Mizar problems as challenges to ATP systems. The service is based on a sound translation from the Mizar language to that of first-order ATP systems, and relies on the recent progress in application of ATP systems in large theories containing tens of thousands of available facts. We present the main features of MizAℝ services, followed by an account of initial experiments in finding proofs with the ATP assistance. Our initial experience indicates that the tool offers substantial help in exploring the Mizar library and in preparing new Mizar articles.

Original languageEnglish (US)
Pages (from-to)229-241
Number of pages13
JournalJournal of Automated Reasoning
Volume50
Issue number2
DOIs
StatePublished - 2013

Fingerprint

Adenosinetriphosphate
Artificial intelligence
Acoustic waves
Experiments

Keywords

  • Automated reasoning
  • Automated reasoning in large theories
  • Interactive theorem proving
  • Mizar

ASJC Scopus subject areas

  • Artificial Intelligence
  • Software
  • Computational Theory and Mathematics

Cite this

ATP and presentation service for Mizar formalizations. / Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoffrey.

In: Journal of Automated Reasoning, Vol. 50, No. 2, 2013, p. 229-241.

Research output: Contribution to journalArticle

Urban, Josef ; Rudnicki, Piotr ; Sutcliffe, Geoffrey. / ATP and presentation service for Mizar formalizations. In: Journal of Automated Reasoning. 2013 ; Vol. 50, No. 2. pp. 229-241.
@article{4ef7cf42857e49c9901863e1052b0630,
title = "ATP and presentation service for Mizar formalizations",
abstract = "This paper describes the Automated Reasoning for Mizar (MizAℝ) service, which integrates several automated reasoning, artificial intelligence, and presentation tools with Mizar and its authoring environment. The service provides ATP assistance to Mizar authors in finding and explaining proofs, and offers generation of Mizar problems as challenges to ATP systems. The service is based on a sound translation from the Mizar language to that of first-order ATP systems, and relies on the recent progress in application of ATP systems in large theories containing tens of thousands of available facts. We present the main features of MizAℝ services, followed by an account of initial experiments in finding proofs with the ATP assistance. Our initial experience indicates that the tool offers substantial help in exploring the Mizar library and in preparing new Mizar articles.",
keywords = "Automated reasoning, Automated reasoning in large theories, Interactive theorem proving, Mizar",
author = "Josef Urban and Piotr Rudnicki and Geoffrey Sutcliffe",
year = "2013",
doi = "10.1007/s10817-012-9269-y",
language = "English (US)",
volume = "50",
pages = "229--241",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "2",

}

TY - JOUR

T1 - ATP and presentation service for Mizar formalizations

AU - Urban, Josef

AU - Rudnicki, Piotr

AU - Sutcliffe, Geoffrey

PY - 2013

Y1 - 2013

N2 - This paper describes the Automated Reasoning for Mizar (MizAℝ) service, which integrates several automated reasoning, artificial intelligence, and presentation tools with Mizar and its authoring environment. The service provides ATP assistance to Mizar authors in finding and explaining proofs, and offers generation of Mizar problems as challenges to ATP systems. The service is based on a sound translation from the Mizar language to that of first-order ATP systems, and relies on the recent progress in application of ATP systems in large theories containing tens of thousands of available facts. We present the main features of MizAℝ services, followed by an account of initial experiments in finding proofs with the ATP assistance. Our initial experience indicates that the tool offers substantial help in exploring the Mizar library and in preparing new Mizar articles.

AB - This paper describes the Automated Reasoning for Mizar (MizAℝ) service, which integrates several automated reasoning, artificial intelligence, and presentation tools with Mizar and its authoring environment. The service provides ATP assistance to Mizar authors in finding and explaining proofs, and offers generation of Mizar problems as challenges to ATP systems. The service is based on a sound translation from the Mizar language to that of first-order ATP systems, and relies on the recent progress in application of ATP systems in large theories containing tens of thousands of available facts. We present the main features of MizAℝ services, followed by an account of initial experiments in finding proofs with the ATP assistance. Our initial experience indicates that the tool offers substantial help in exploring the Mizar library and in preparing new Mizar articles.

KW - Automated reasoning

KW - Automated reasoning in large theories

KW - Interactive theorem proving

KW - Mizar

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

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

U2 - 10.1007/s10817-012-9269-y

DO - 10.1007/s10817-012-9269-y

M3 - Article

AN - SCOPUS:84875991525

VL - 50

SP - 229

EP - 241

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 2

ER -