Theorem Proving by Incrementally Extending Theorem Domain

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, the authors 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.

Provided by: International Journal of Emerging Trends & Technology in Computer Science (IJETTCS) Topic: Software Date Added: Feb 2015 Format: PDF

Find By Topic