ConProve: A conceptual prover system

Abstract

ConProve is an automated prover for propositional logic. It takes, as an input, a set of propositional formulas and proves whether a goal holds or not. ConProve converts each formula to its corresponding Truth Table Binary Relation (TTBR) considered also as a formal context (FC). The objects in FC correspond to all possible formulas interpretations (in terms of their truth value assignments), and the properties in FC correspond to the terms. When the function the 'BuildContext' function, ConProve starts the new goal proving. Firstly, it adds the goal negation to the set of formulas and constructs the formal contexts (FCs) relating formulas to terms. Secondly, it makes the FCs grouping and deduces, based on the conceptual reasoning, if the goal holds. The tool offers a user-friendly interface allowing the editing of the set of formulas as well as the visualization of the reasoning steps. Besides the tool, the paper illustrates the importance of the conceptual reasoning in deriving new conclusions as well as in discovering new, possibly implications by applying the extended Galois Connection.