ATP and presentation service for Mizar formalizations

DOI10.1007/s10817-012-9269-yzbMath1260.68380arXiv1109.0616OpenAlexW2399753239MaRDI QIDQ1945905

Geoff Sutcliffe, Piotr Rudnicki, Josef Urban

Publication date: 17 April 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1109.0616

zbMATH Keywords

automated reasoninginteractive theorem proving\texttt{Mizar}automated reasoning in large theories

Mathematics Subject Classification ID

Related Items (32)

Pappus's hexagon theorem in real projective plane ⋮ On weakly associative lattices and near lattices ⋮ Proof mining with dependent types ⋮ Four decades of {\textsc{Mizar}}. Foreword ⋮ Mechanizing complemented lattices within Mizar type system ⋮ MizAR 40 for Mizar 40 ⋮ Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver ⋮ A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description) ⋮ Mining the Archive of Formal Proofs ⋮ Mizar: State-of-the-art and Beyond ⋮ A learning-based fact selector for Isabelle/HOL ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Pascal's theorem in real projective plane ⋮ VizAR: visualization of automated reasoning proofs (system description) ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ An integrated web platform for the Mizar Mathematical Library ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Flexary connectives in Mizar ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Formalization of Euler-Lagrange equation set based on variational calculus in HOL light ⋮ TacticToe: learning to prove with tactics ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ On two alternative axiomatizations of lattices by McKenzie and Sholander ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description ⋮ SAT-Enhanced Mizar Proof Checking ⋮ Theorem proving as constraint solving with coherent logic ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Premise selection for mathematics by corpus analysis and kernel methods ⋮ Formalization of quasilattices

Uses Software

• MizarMode
• MPTP 0.2
• Metis_
• Mizar
• MML
• Sledgehammer
• MaLARea
• SystemOnTPTP
• seL4
• kepler98

Cites Work

• Unnamed Item
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• MPTP 0.2: Design, implementation, and initial experiments
• Lightweight relevance filtering for machine-generated resolution problems
• Premise selection for mathematics by corpus analysis and kernel methods
• A proof of the Kepler conjecture
• Simple Graphs as Simplicial Complexes: the Mycielskian of a Graph
• Automated Proof Compression by Invention of New Definitions
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
• Sine Qua Non for Large Theory Reasoning
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
• Sur le coloriage des graphs
• Mathematical Knowledge Management

This page was built for publication: ATP and presentation service for Mizar formalizations