How to identify, translate and combine logics?

DOI10.1093/LOGCOM/EXU079MaRDI QIDQ3133182zbMATH OpenOpenAlexFDO

Authors Florian Rabe

Publication date 13 February 2018

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/ec44ceb5b2c5da6814a230f8af0ac5bc5c045b94

Mathematics Subject Classification ID

Combined logics (03B62) Logic in computer science (03B70) Categorical logic, topoi (03G30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A logical framework combining model and proof theory
• scientific article; zbMATH DE number 753781
• Equivalences between logics and their representing type theories
• scientific article; zbMATH DE number 2110615
• Towards logical frameworks in the heterogeneous tool set Hets

Cited in

(19)

• Making PVS accessible to generic services by interpretation in a universal format
• Logic-independent proof search in logical frameworks (short paper)
• Structuring theories with implicit morphisms
• Structure-preserving diagram operators
• Mathematical models as research data via flexiformal theory graphs
• Morphism axioms
• The future of logic: foundation-independence
• Generic literals
• Formal logic definitions for interchange languages
• scientific article; zbMATH DE number 753781 (Why is no real title available?)
• Lax theory morphisms
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• scientific article; zbMATH DE number 7756106 (Why is no real title available?)
• Combining higher-order logic with set theory formalizations
• Formal Reasoning Using Distributed Assertions
• A logical framework perspective on conservativity
• Rapid prototyping formal systems in MMT: 5 case studies
• Systematic translation of formalizations of type theory from intrinsic to extrinsic style
• Soundness-preserving fusion of modal logics in Coq

Describes a project that uses

Uses Software

• MMT

This page was built for publication: How to identify, translate and combine logics?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3133182)