Robinson Arithmetic

Andrei Popescu and Dmitriy Traytel

16 September 2020

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.
BSD License

Depends On

Topics

Related Entries

Theories

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{http://isa-afp.org/entries/Robinson_Arithmetic.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download