### 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

- Logic/Proof theory

### Session Robinson_Arithmetic

- Robinson_Arithmetic
- Instance

### Depends on

- Nominal 2
- Syntax-Independent Logic Infrastructure

## Cite

×

Robinson_Arithmetic-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Sep 18, 2020 : Isabelle2020