A domain-independent system for modeling number theory using first-order predicate logic

Many existing theorem provers employ domain-dependent knowledge in their aim to model the reasoning methods of mathematics. Hoping to achieve the same objective in a better way, the present work seeks to provide a domain-independent system of theorems for modeling number theory using first-order predicate calculus. This system is based on the definition of natural numbers that is used in the Peano Arithmetic. It is meant as a theoretical tool for mathematicians, as opposed to the existing computational tools. Proofs to theorems of this system were attempted by TGTP (The Great Theorem Prover), a resolution-refutation based theorem prover. Performance analysis of this prover on those theorems is presented at the end.