Robinson Arithmetic

Andrei Popescu 🌐 and Dmitriy Traytel 🌐

September 16, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We instantiate our syntax-independent logic infrastructure developed in a separate AFP entry to the FOL theory of Robinson arithmetic (also known as Q). The latter was formalised using Nominal Isabelle by adapting Larry Paulson’s formalization of the Hereditarily Finite Set theory.

License

BSD License

Topics

Session Robinson_Arithmetic

Depends on

Cite

× 
@article{Robinson_Arithmetic-AFP,
  author  = {Andrei Popescu and Dmitriy Traytel},
  title   = {Robinson Arithmetic},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/Robinson_Arithmetic.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: