Robinson arithmetic swMATH ID: 42008 Software Authors: Popescu, A., Traytel, D. Description: afp Robinson_Arithmetic. Robinson Arithmetic: 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. Homepage: https://www.isa-afp.org/entries/Robinson_Arithmetic.html Dependencies: Isabelle Related Software: Archive Formal Proofs; Locales; Isabelle/HOL; Coq; GitHub; Eisbach; Nominal Isabelle; HOLyHammer; NQTHM; Sledgehammer; HOL Light; AVATAR; Saturation_Framework; Ordered_Resolution_Prover; Nested Multisets; Logtk; Superposition Calculus; DISCOUNT; CeTA; Isabelle/jEdit Cited in: 2 Publications Cited by 5 Authors 2 Traytel, Dmitry 1 Blanchette, Jasmin Christian 1 Popescu, Andrei 1 Schlichtkrull, Anders 1 Waldmann, Uwe Cited in 1 Serial 2 Journal of Automated Reasoning Cited in 2 Fields 2 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year