Previous Issues
Volume :26 Issue : 1 1999
Add To Cart
Download
A domain-independent system for modeling number theory using first-order predicate logic
Auther : MOHAMMED ALMULLA AND L.A-M. HANNA
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.