Metamorphic Testing of Logic Theorem Prover

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.

ArchitectECA2030 receives funding within the Electronic Components and Systems For European Leadership Joint Undertaking (ESCEL JU) in collaboration with the European Union’s Horizon2020 Framework Programme and National Authorities, under grant agreement n$^\circ$ 877539. The work was partially funded by the Austrian Federal Ministry of Climate Action, Environment, Energy, Mobility, Innovation and Technology (BMK) under the program “ICT of the Future” project 877587.