Theorem proving by incrementally extending theorem domain
Ismail A. Ismail, Mohamed M. Awad · 2015
Automated Theorem provers are used to check if the mathematical theorems are proved true or false. If the theorem is true, the automated theorem prover, usually, prints out the proof. In this paper we present a new approach to deal with the other case, i.e. if the theorem is false. The semantic tableau method is used to extend the theorem domain. The modified automated theorem prover suggests an extension of the domain, if it is available, to present a new provable theorem.