The future of logic: foundation-independence

DOI10.1007/S11787-015-0132-XMaRDI QIDQ263104zbMATH OpenOpenAlexFDO

Authors Florian Rabe

Publication date 4 April 2016

Published in Logica Universalis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11787-015-0132-x

zbMATH Keywords

presentationproof theorysearchknowledge managementlogical declarationsMMTmodel theoryparsingsyntaxtheorytheory morphismtype reconstructionuser interface

Mathematics Subject Classification ID

Higher-order logic (03B16) Abstract deductive systems (03B22) Logic in computer science (03B70)

Recommendations

• How to identify, translate and combine logics?
• A logical framework combining model and proof theory
• A scalable module system
• Types for Proofs and Programs
• A Modular Type Reconstruction Algorithm

Cites work

• A Search Engine for Mathematical Formulae
• A framework for defining logics
• A scalable module system
• Combinatory logic. With two sections by William Craig.
• Crafting a Proof Assistant
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Formalising foundations of mathematics
• Generic literals
• How to identify, translate and combine logics?
• Institution-independent model theory
• Institutions: abstract model theory for specification and programming
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Lax theory morphisms
• Logical frameworks
• Project abstract: logic atlas and integrator (LATIN)
• Representing model theory in a type-theoretical logical framework
• System description: MathHub.info
• The MMT API: a generic MKM system
• The Mizar Mathematical Library in OMDoc: translation and applications
• Tools and algorithms for the construction and analysis of systems. 13th international conference, TACAS 2007, held as part of the joint European conferences on theory and practice of software, ETAPS 2007, Braga, Portugal, March 24 -- April 1, 2007. Procee
• Towards Knowledge Management for HOL Light

Cited in

(5)

• Isabelle/HOL/GST: a formal proof environment for generalized set theories
• scientific article; zbMATH DE number 6297875 (Why is no real title available?)
• ON EXISTENTIAL DECLARATIONS OF INDEPENDENCE IN IF LOGIC
• Formal Reasoning Using Distributed Assertions
• A semantic framework for proof evidence

Describes a project that uses

Uses Software

• MathML
• kepler98
• LATIN
• seL4
• MathHub.info
• OMDoc
• QMT
• MMT
• Twelf
• Nuprl
• HOL Light
• HOL
• Mizar
• MathWebSearch
• PVS
• Isabelle/HOL
• Isabelle
• Coq

This page was built for publication: The future of logic: foundation-independence

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