Project abstract: logic atlas and integrator (LATIN)

DOI10.1007/978-3-642-22673-1_24MaRDI QIDQ5200129zbMATH OpenOpenAlexDBLPWikidataFDO

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

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Recommendations

• Formalising foundations of mathematics
• Towards logical frameworks in the heterogeneous tool set Hets
• Formal logic definitions for interchange languages
• A logical framework combining model and proof theory
• scientific article; zbMATH DE number 1231668

Cites work

• A logical framework combining model and proof theory
• A scalable module system
• Formalising foundations of mathematics
• Institutions: abstract model theory for specification and programming
• Integrating Web Services into Active Mathematical Documents
• Representing model theory in a type-theoretical logical framework
• Towards MKM in the large: modular representation and scalable software architecture
• Towards logical frameworks in the heterogeneous tool set Hets

Cited in

(18)

• The future of logic: foundation-independence
• A scalable module system
• Math Literate Knowledge Management via Induced Material
• 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
• The Mizar Mathematical Library in OMDoc: translation and applications
• Classification of alignments between concepts of formal mathematical systems
• Lax theory morphisms
• 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
• A Maude environment for CafeOBJ
• System description: MathHub.info

Describes a project that uses

Uses Software

• LATIN
• TNTBase
• MMT
• Hets
• Twelf
• Isabelle

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)