Project abstract: logic atlas and integrator (LATIN)
From MaRDI portal
Publication:5200129
DOI10.1007/978-3-642-22673-1_24zbMATH Open1278.68285DBLPconf/mkm/CodescuHKMR11OpenAlexW1487612545WikidataQ57389385 ScholiaQ57389385MaRDI QIDQ5200129FDOQ5200129
Authors: Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe 
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22673-1_24
Recommendations
Cites Work
- Formalising foundations of mathematics
- A scalable module system
- Institutions: abstract model theory for specification and programming
- Representing model theory in a type-theoretical logical framework
- Towards logical frameworks in the heterogeneous tool set Hets
- Towards MKM in the large: modular representation and scalable software architecture
- Integrating Web Services into Active Mathematical Documents
- A logical framework combining model and proof theory
Cited In (18)
- The future of logic: foundation-independence
- Math Literate Knowledge Management via Induced Material
- A scalable module system
- Representing model theory in a type-theoretical logical framework
- Parchments for CafeOBJ logics
- Formal logic definitions for interchange languages
- Structure-preserving diagram operators
- A data model and encoding for a semantic, multilingual terminology of mathematics
- A query language for formal mathematical libraries
- Lax theory morphisms
- The Mizar Mathematical Library in OMDoc: translation and applications
- Classification of alignments between concepts of formal mathematical systems
- Logic-independent proof search in logical frameworks (short paper)
- Semantics of \textsc{OpenMath} and \textsc{MathML3}
- Experiences from exporting major proof assistant libraries
- Structuring theories with implicit morphisms
- System description: MathHub.info
- A Maude environment for CafeOBJ
Uses Software
This page was built for publication: Project abstract: logic atlas and integrator (LATIN)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5200129)
