Metamorphic Testing of Logic Theorem Prover
Oliver A. Tazl, Franz Wotawa
Abstract: The use of Artificial Intelligence methodologies including machine learning for object recognition and other tasks as well as reasoning has recently gained more attention. This is due to the fact of applications like autonomous driving but also apps for providing recommendations or schedules. In this paper, we focus on testing applications utilizing logic theorem proving for implementing their functionalities. Testing logic theorem prover is important in order to assure that the obtained results are correct and complete as specified. We show how metamorphic testing can be used in this context. In particular, the proposed method takes a logic sentence and modifies it without changing its logical status, i.e., satisfiability. The testing method can be applied to assure the correctness of reasoning via generating logic sentences of arbitrary sizes, but also for performance testing. We applied the presented testing method to 2 different theorem provers and report on obtained results.
