Previous Issues

Department of Mathematics and Computer Science, Kuwait University, P.O. B0X 5969, Safat 13060 Kuwait. E-mail:  almulla@sci.kuniv.edu.kw & hannalam@sci.kuniv.edu.kw

ABSTRACT

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.