Assertion-level proof representation with under-specification

MaRDI QIDQ2847390zbMATH OpenFDO

Authors Serge Autexier, Christoph Benzmüller, Armin Fiedler, Helmut Horacek, Bao Quoc Vo

Publication date 9 September 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066104000118

Mathematics Subject Classification ID

Knowledge representation (68T30)

Recommendations

• Reconstructing proofs at the assertion level
• Mathematical Knowledge Management
• scientific article; zbMATH DE number 3922016
• Presenting machine-found proofs
• Mechanizing Mathematical Reasoning

Cited in

(6)

• Formal justification of underspecification for S5
• Semi-intelligible Isar proofs from machine-generated proofs
• Proving correctness w.r.t. specifications with hidden parts
• A proof-centric approach to mathematical assistants
• Computer supported mathematics with MEGA
• Supporting the formal verification of mathematical texts

Describes a project that uses

Uses Software

• Isar
• OMEGA

This page was built for publication: Assertion-level proof representation with under-specification

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