oa Conceptual reasoning for consistency insurance in logical deduction and application for critical systems

Reasoning in propositional logic is a key element in software engineering; it is applied in different domains, e.g: specification validation, code checking, theorem proving, etc. Since reasoning is a basic component in the analysis and verification of different critical systems, significant efforts have been dedicated to improve its efficiency in terms of time complexity, correctness and generalization to new problems support (e.g., SAT- Problem, Inference-Rules, inconsistency detection, etc.). We propose a new Conceptual Reasoning Method for an inference engine in which such improvements will be achieved by the combination of the semantic interpretations of a logical formula and the formal concept analysis mathematical background. In fact, each logical formula is mapped into a truth table formal context and any logical deduction is obtained by Galois connection. More particularly, we combine all truth tables into a global one which has the advantage of containing the complete knowledge of all deducible rules or, possibly, an eventual inconsistency in the whole system. A first version of the new reasoning system was implemented and applied for medical data. Efficiency in conflicts resolutions as well as in knowledge expressiveness and reasoning were shown. Serious challenges related with time complexity have been faced out and still more improvements are under investigation. "Acknowledgement: This publication was made possible by a grant from the Qatar National Research Fund NPRP04-1109-1-174. Its contents are solely the responsibility of the authors and do not necessarily represent the official views of the QNRF."