Eliciting implicit assumptions of Mizar proofs by property omission
From MaRDI portal
Publication:1945901
DOI10.1007/s10817-012-9264-3zbMath1260.68361arXiv1109.0633MaRDI QIDQ1945901
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.0633
formal proofs; proof analysis; proof assistants; interactive theorem proving; \texttt{Mizar}; implicit assumptions; large formal libraries; proof dependencies
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- MPTP 0.2: Design, implementation, and initial experiments
- Obvious inferences
- Large Formal Wikis: Issues and Solutions
- Mathematical Knowledge Management
- Fast LCF-Style Proof Reconstruction for Z3
- Mathematical Knowledge Management