Main Article Content
Abstract
Proving by resolution method is one of methods which can be used to prove the logical statement
according to given statements. To automate the proving process and to support the teaching-learning process of
discrete mathematics course in the university, this proving can be done with the aid of computer software. To
enable the effective use of software, the error handler facilities are added. They help users to overcome
erroneous inputs and therefore facilitate the use of software.
In this paper, several possibilities of mistaken input performed by users are elaborated. By analyzing
them, the error handler facilities are added in the software for proving the propositional logic statement by
using resolution method. According to the testing which was performed, the error handler facilities can be
applied in the software.
Keywords: Resolution, Conjunctive Normal Form, Automated Reasoning, Handling Errors.