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

Citations by Year