DLS-Forgetter: An Implementation of the DLS Forgetting Calculus for First-Order Logic

DLS-Forgetter is a reasoning tool that aims to compute restricted views of a knowledge base of first-order logic formulae via semantic forgetting. Semantic forgetting achieves this by eliminating predicate symbols in an equivalence preserving way up to the remain- ing symbols. Forgetting has many applications such as information hiding, explanation generation and computing logical difference. DLS-Forgetter combines ideas from two Ackermann-based approaches: the DLS algorithm and a modal logic inference system inspired by the algorithm. The tool enhances the DLS algorithm by incorporating an ordering over the symbols in the forgetting signature. This allows more control over the forgetting process and the application of the elimination rules. The theory behind the tool is provided by a first-order Ackermann calculus, a first-order generalisation of the rules outlined by the modal logic inference system. The purpose of the tool is to provide the research community with an experimental tool to allow further research to be conducted in the area. This paper describes the DLS-Forgetter tool along with its underlying calculus, it outlines the forgetting process used in the implementation, and presents results of an empirical evaluation.