Robinson Arithmetic

 

Title: Robinson Arithmetic
Authors: Andrei Popescu and Dmitriy Traytel
Submission date: 2020-09-16
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.
BibTeX:
@article{Robinson_Arithmetic-AFP,
  author  = {Andrei Popescu and Dmitriy Traytel},
  title   = {Robinson Arithmetic},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2020,
  note    = {\url{http://isa-afp.org/entries/Robinson_Arithmetic.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Nominal2, Syntax_Independent_Logic