Eliciting implicit assumptions of Mizar proofs by property omission

DOI10.1007/S10817-012-9264-3zbMATH Open1260.68361arXiv1109.0633OpenAlexW3122106493MaRDI QIDQ1945901FDOQ1945901

Authors: Jesse Alama 

Publication date: 17 April 2013

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

Abstract: When formalizing proofs with interactive theorem provers, it often happens that extra background knowledge (declarative or procedural) about mathematical concepts is employed without the formalizer explicitly invoking it, to help the formalizer focus on the relevant details of the proof. In the contexts of producing and studying a formalized mathematical argument, such mechanisms are clearly valuable. But we may not always wish to suppress background knowledge. For certain purposes, it is important to know, as far as possible, precisely what background knowledge was implicitly employed in a formal proof. In this note we describe an experiment conducted on the MIZAR Mathematical Library of formal mathematical proofs to elicit one such class of implicitly employed background knowledge: properties of functions and relations (e.g., commutativity, asymmetry, etc.).

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

Recommendations

• Custom automations in Mizar
• mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Enhancement of \textsc{Mizar} texts with transitivity property of predicates
• MPTP-motivation, implementation, first experiments

zbMATH Keywords

proof analysisinteractive theorem provingproof assistantsformal proofs\texttt{Mizar}implicit assumptionslarge formal librariesproof dependencies

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• MPTP 0.2: Design, implementation, and initial experiments
• Subsystems of second order arithmetic
• Obvious inferences
• Mathematical Knowledge Management
• Fast LCF-Style Proof Reconstruction for Z3
• Mathematical Knowledge Management
• Title not available (Why is that?)
• Language, proof, and logic. In collaboration with Albert Liu, Michael Murray and Emma Pease. With CD-ROM
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• Large formal wikis: issues and solutions

Cited In (2)

• Title not available (Why is that?)
• Mizar: state-of-the-art and beyond

Uses Software

• MPTP 0.2
• Mizar
• LPL software
• z3
• MML
• Tipi
• mizar-items

This page was built for publication: Eliciting implicit assumptions of Mizar proofs by property omission

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1945901)