Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
type: Item
instance of: scholarly article
title: Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
author: Andrei Popescu
author: Dmitriy Traytel
published in: Journal of Automated Reasoning
publication date: 2021-11-24T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7433027
zbMATH Keywords: Gödel's incompleteness theorems
zbMATH Keywords: abstract requirements
zbMATH Keywords: formal verification
zbMATH Keywords: proof assistant
zbMATH Keywords: Isabelle/HOL
describes a project that uses: HOL Light
describes a project that uses: Robinson arithmetic
describes a project that uses: Coq
describes a project that uses: Archive Formal Proofs
describes a project that uses: Isabelle/HOL
describes a project that uses: Sledgehammer
describes a project that uses: NQTHM
describes a project that uses: HOLyHammer
describes a project that uses: Nominal Isabelle
describes a project that uses: Locales
describes a project that uses: Eisbach
describes a project that uses: GitHub
MaRDI profile type: Publication
Wikidata QID: Q113901237
full work available at URL: s10817-021-09599-8
OpenAlex ID: W3196549399
cites work: Locales: a module system for mathematical theories
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Unified Classical Logic Completeness
cites work: Q4397069
cites work: The scope of Gödel's first incompleteness theorem
cites work: Abstract proof checking: An example motivated by an incompleteness theorem
cites work: Q5573370
cites work: Q4830809
cites work: Institution-independent model theory
cites work: Nominal (Universal) Algebra: Equational Logic with Names and Binding
cites work: Institutions: abstract model theory for specification and programming
cites work: Q3618853
cites work: HOL Light: An Overview
cites work: Q5772177
cites work: Redundancies in the Hilbert-Bernays derivability conditions for Gödel's second incompleteness theorem
cites work: HOL(y)Hammer: online ATP service for HOL Light
cites work: GENERALIZATIONS OF GÖDEL’S INCOMPLETENESS THEOREMS FOR ∑n-DEFINABLE THEORIES OF ARITHMETIC
cites work: Q5328115
cites work: A Consistent Foundation for Isabelle/HOL
cites work: Comprehending Isabelle/HOL’s Consistency
cites work: From types to sets by local type definition in higher-order logic
cites work: Solution of a problem of Leon Henkin
cites work: Eisbach: a proof method language for Isabelle
cites work: Concrete Semantics
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Theorem Proving in Higher Order Logics
cites work: Q5219927
cites work: A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
cites work: A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
cites work: Term-generic logic
cites work: A formally verified abstract account of Gödel's incompleteness theorems
cites work: Automated proofs of Löb's theorem and Gödel's two incompleteness theorems
cites work: Formalizing Bachmair and Ganzinger's ordered resolution prover
cites work: Metamathematics, Machines and Gödel's Proof
cites work: Automated search for Gödel's proofs
cites work: Self-reference and modal logic
cites work: Q4003735
cites work: Finite sets and Gödel's incompleteness theorems
cites work: Q4040000
cites work: Undecidable theories
cites work: Nominal techniques in Isabelle/HOL
DOI: 10.1007/S10817-021-09599-8
description: scientific article; zbMATH DE number 7433027