Computer Science – Logic in Computer Science
Scientific paper
2011-09-03
Computer Science
Logic in Computer Science
11 pages, 3 tables. Preliminary version presented at the 3rd Workshop on Modules and Libraries for Proof Assistants (MLPA-11),
Scientific paper
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.).
No associations
LandOfFree
Eliciting implicit assumptions of proofs in the MIZAR Mathematical Library by property omission does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Eliciting implicit assumptions of proofs in the MIZAR Mathematical Library by property omission, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Eliciting implicit assumptions of proofs in the MIZAR Mathematical Library by property omission will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-148116