A Foundational View on Integration Problems
From MaRDI portal
Publication:5200111
DOI10.1007/978-3-642-22673-1_8zbMath1278.68289DBLPconf/mkm/RabeKC11arXiv1105.2725OpenAlexW3102983490WikidataQ57389379 ScholiaQ57389379MaRDI QIDQ5200111
Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1105.2725
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics ⋮ Math Literate Knowledge Management via Induced Material ⋮ A scalable module system ⋮ Semantics of \textsc{OpenMath} and \textsc{MathML3} ⋮ Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach ⋮ Towards Knowledge Management for HOL Light
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A scalable module system
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A Skeptic's approach to combining HOL and Maple
- May I borrow your logic? (Transporting logical structures along maps)
- Dealing with algebraic expressions over a field in Coq using Maple
- Translating higher-order clauses to first-order clauses
- Formalising foundations of mathematics
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Towards MKM in the Large: Modular Representation and Scalable Software Architecture
- An Interpretation of Isabelle/HOL in HOL Light
- A framework for defining logics
- Institutions: abstract model theory for specification and programming
- Automated Reasoning
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Types for Proofs and Programs
- Importing HOL Light into Coq
- A Mechanized Translation from Higher-Order Logic to Set Theory
This page was built for publication: A Foundational View on Integration Problems
