Show simple item record

AuthorElloumi, Samir
AuthorJaoua, Ali
AuthorBoulifa, Bilel
AuthorSaleh, Mohammad
AuthorAl Otaibi, Jameela
Available date2016-05-01T13:32:01Z
Publication Date2014
Publication NameProceedings of IEEE/ACS International Conference on Computer Systems and Applications, AICCSA
CitationS. Elloumi, A. Jaoua, B. Boulifa, M. Saleh and J. A. Otaibi, "ConProve: A conceptual prover system," 2014 IEEE/ACS 11th International Conference on Computer Systems and Applications (AICCSA), Doha, 2014, pp. 647-651.
AbstractConProve 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.
SponsorQatar National Research Fund NPRP 04-1109-1-174.
SubjectConceptual reasoning and proving
SubjectFormal contexts combining
SubjectInference Engine
SubjectTruth Table Binary Relation
TitleConProve: A conceptual prover system
TypeConference Paper
Volume Number2014

Files in this item


There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record