The future of logic: foundation-independence

DOI10.1007/S11787-015-0132-XzbMATH Open1436.03179OpenAlexW2300316091MaRDI QIDQ263104FDOQ263104

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

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

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)

Cites Work

• The MMT API: A Generic MKM System
• A Search Engine for Mathematical Formulae
• System Description: MathHub.info
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• 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. Proceedings.
• Institution-independent model theory
• Logical frameworks
• Formalising foundations of mathematics
• How to identify, translate and combine logics?
• Generic Literals
• Crafting a Proof Assistant
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A scalable module system
• A framework for defining logics
• Institutions: abstract model theory for specification and programming
• Project Abstract: Logic Atlas and Integrator (LATIN)
• Lax Theory Morphisms
• Towards Knowledge Management for HOL Light
• Representing model theory in a type-theoretical logical framework
• Combinatory logic. With two sections by William Craig.

Cited In (5)

• Title not available (Why is that?)
• ON EXISTENTIAL DECLARATIONS OF INDEPENDENCE IN IF LOGIC
• Formal Reasoning Using Distributed Assertions
• A semantic framework for proof evidence
• Isabelle/HOL/GST: a formal proof environment for generalized set theories

Uses Software

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

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)