×

zbMATH — the first resource for mathematics

A domain-independent system for modeling number theory using first-order predicate logic. (English. Arabic summary) Zbl 1207.68336
Summary: Many exdisting 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 modelling 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.
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03F30 First-order arithmetic and fragments
Software:
HERBY; OTTER; TGTP; TPTP
PDF BibTeX XML Cite