A scalable module system

DOI10.1016/j.ic.2013.06.001zbMath1358.68283OpenAlexW1999680561WikidataQ57389341 ScholiaQ57389341MaRDI QIDQ391632

Michael Kohlhase, Florian Rabe

Publication date: 10 January 2014

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2013.06.001

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Knowledge representation (68T30)

Related Items (38)

LF+ in Coq for "fast and loose" reasoning ⋮ Lax Theory Morphisms ⋮ Mathematical models as research data via flexiformal theory graphs ⋮ A web-based toolkit for mathematical word processing applications with semantics ⋮ Formalizing mathematical knowledge as a biform theory graph: a case study ⋮ Classification of alignments between concepts of formal mathematical systems ⋮ A new export of the Mizar mathematical library ⋮ Generic Literals ⋮ A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics ⋮ Formal Logic Definitions for Interchange Languages ⋮ Math Literate Knowledge Management via Induced Material ⋮ A Query Language for Formal Mathematical Libraries ⋮ Theory Presentation Combinators ⋮ Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge ⋮ Structuring theories with implicit morphisms ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ Morphism equality in theory graphs ⋮ Extracting theory graphs from Aldor libraries ⋮ Injecting formal mathematics into LaTeX ⋮ System description STEX3 -- a \LaTeX-based ecosystem for semantic/active mathematical documents ⋮ The Mizar Mathematical Library in OMDoc: translation and applications ⋮ Semantics of \textsc{OpenMath} and \textsc{MathML3} ⋮ Unnamed Item ⋮ Structure-preserving diagram operators ⋮ A Foundational View on Integration Problems ⋮ Combining Source, Content, Presentation, Narration, and Relational Representation ⋮ Project Abstract: Logic Atlas and Integrator (LATIN) ⋮ Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach ⋮ The SMGloM Project and System: Towards a Terminology and Ontology for Mathematics ⋮ Spreadsheet Interaction with Frames: Exploring a Mathematical Practice ⋮ Compensating the Computational Bias of Spreadsheets with MKM Techniques ⋮ Experiences from exporting major proof assistant libraries ⋮ A Data Model and Encoding for a Semantic, Multilingual Terminology of Mathematics ⋮ Realms: A Structure for Consolidating Knowledge about Mathematical Theories ⋮ Flexary Operators for Formalized Mathematics ⋮ Towards Knowledge Management for HOL Light ⋮ System Description: MathHub.info ⋮ The future of logic: foundation-independence

Uses Software

• Coq
• Isabelle
• CASL
• MAYA
• PVS
• TPTP
• Mizar
• OBJ3
• Maude
• SCSCP
• Twelf
• Hets
• Automath
• MMT
• QMT
• OMDoc
• TNTBase
• STEXIDE
• IMPS
• Locales
• LATIN
• MathML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Representing model theory in a type-theoretical logical framework
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The calculus of constructions
• Specifications in an arbitrary institution
• The TPTP problem library. CNF release v1. 2. 1
• IMPS: An interactive mathematical proof system
• Structured theory presentations and logic representations
• Isabelle. A generic theorem prover
• CASL reference manual. The complete documentation of the common algebraic specification language.
• The Mizar Mathematical Library in OMDoc: translation and applications
• Development graphs -- proof management for structured specifications
• A Universal Machine for Biform Theory Graphs
• A Proof Theoretic Interpretation of Model Theoretic Hiding
• Towards Logical Frameworks in the Heterogeneous Tool Set Hets
• Extending MKM Formats at the Statement Level
• A Query Language for Formal Mathematical Libraries
• Formalising foundations of mathematics
• Packaging Mathematical Structures
• Towards a mechanized metatheory of standard ML
• An Integrated Development Environment for Collections
• Towards MKM in the Large: Modular Representation and Scalable Software Architecture
• Crafting a Proof Assistant
• Integrating Web Services into Active Mathematical Documents
• OpenMath in SCIEnce: SCSCP and POPCORN
• A framework for defining logics
• Institutions: abstract model theory for specification and programming
• A Foundational View on Integration Problems
• Project Abstract: Logic Atlas and Integrator (LATIN)
• A logical framework combining model and proof theory
• Notations for Living Mathematical Documents
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES

This page was built for publication: A scalable module system