The Pocket Reasoner -- Automatic Reasoning on Small Devices

Abstract

Automated reasoning in classical first-order logic is a core research field in Artificial Intelligence. Most of the fully automated reasoning tools are large and complex systems implementing proof search methods that have significant memory requirements. This paper presents an automated reasoning tool implemented on an iPod Nano. It is based on leanCoP, a very compact Prolog implementation of the connection calculus, which operates on the structure of the given formula without generating new subformula instances. Hence, the memory requirements are significantly lower, allowing leanCoP to run on devices with only little (random-access) memory. The paper presents details of the proof search calculus, its implementation, and a practical evaluation of the presented reasoning tool.