A Foundational View on Integration Problems
From MaRDI portal
Publication:5200111
DOI10.1007/978-3-642-22673-1_8zbMath1278.68289arXiv1105.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
Symbolic computation and algebraic computation (68W30) Logic in artificial intelligence (68T27) Knowledge representation (68T30)
Related Items
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
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
