Robinson arithmetic (Q5972508)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Robinson_Arithmetic
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Robinson arithmetic |
AFP entry Robinson_Arithmetic |
Statements
Andrei Popescu
0 references
Dmitriy Traytel
0 references
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 .
0 references
16 September 2020
0 references
Robinson Arithmetic (English)
0 references
