A sound and complete CG proof procedure combining projections with analytic tableaux

Abstract

Conceptual Graphs offer an attractive and intuitive formalism for knowledge representation in Artificial Intelligence. The formalism calls for efficient systems of reasoning. Projection is one such tool for a language limited to conjunction and existential quantification (Simple Conceptual Graphs). Projection is very efficient for certain classes of Conceptual Graphs and offers an original approach to deduction: the perspective of graph matching. The aim of this paper is twofold: Propose an efficient analytic deduction system that combines analytic tableaux with projection for a language of Conceptual Graphs extended to all non functional First-Order Logic formulae and compare this method with the one introduced in [1] for Simple Conceptual Graph rules.