Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] A bundle of ATP entries

view this post on Zulip Email Gateway (Sep 18 2020 at 14:45):

From: Lawrence Paulson <>
I’m delighted to announce a new entry by Andrei Popescu and Dmitriy Traytel:

Syntax-Independent Logic Infrastructure

We formalize a notion of logic whose terms and formulas are kept abstract. In particular, logical connectives, substitution, free variables, and provability are not defined, but characterized by their general properties as locale assumptions. Based on this abstract characterization, we develop further reusable reasoning infrastructure. For example, we define parallel substitution (along with proving its characterizing theorems) from single-point substitution. Similarly, we develop a natural deduction style proof system starting from the abstract Hilbert-style one. These one-time efforts benefit different concrete logics satisfying our locales' assumptions. We instantiate the syntax-independent logic infrastructure to Robinson arithmetic (also known as Q) in the AFP entry Robinson_Arithmetic and to hereditarily finite set theory in the AFP entries Goedel_HFSet_Semantic and Goedel_HFSet_Semanticless, which are part of our formalization of Gödel's Incompleteness Theorems described in our CADE-27 paper A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.

And built upon that, four additional entries:

An Abstract Formalization of Gödel's Incompleteness Theorems
From Abstract to Concrete Gödel's Incompleteness Theorems—Part I
From Abstract to Concrete Gödel's Incompleteness Theorems—Part II
Robinson Arithmetic

An impressive body of work!

Larry Paulson

Last updated: Jan 25 2022 at 02:35 UTC