Automatically finding theory morphisms for knowledge management

DOI10.1007/978-3-319-96812-4_18MaRDI QIDQ1798969zbMATH OpenOpenAlexFDO

Authors Dennis Müller, Michael Kohlhase, Florian Rabe

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-96812-4_18

Mathematics Subject Classification ID

Knowledge representation (68T30)

Recommendations

• Structuring theories with implicit morphisms
• Enhanced Theorem Reuse by Partial Theory Inclusions
• Matching concepts across HOL libraries
• scientific article; zbMATH DE number 2003150
• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system

Cited in

(3)

• scientific article; zbMATH DE number 7756106 (Why is no real title available?)
• Structuring theories with implicit morphisms
• Morphism equality in theory graphs

Describes a project that uses

Uses Software

• TGView
• OpenDreamKit
• IMPS
• PVS
• Isabelle

This page was built for publication: Automatically finding theory morphisms for knowledge management

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