Conceptual graphs and first order logic

We study Sowa's conceptual graphs (CGs) with both existential and universal quantifiers. We explore in detail the existential fragment. We extend and modify Sowa's original graph derivation system with new rules and prove the soundness and completeness theorem with respect to Sowa's standard interpr etation of CGs into first order logic (FOL), The proof is obtained by reduc ing the graph derivation to a question-answering problem. The graph derivat ion can be equivalently obtained by querying a Definite Horn Clauses progra m by a conjunction of positive atoms. Moreover, the proof provides an algor ithm for graph derivation in a pure proof-theoretic fashion, namely by mean s of a slight enhancement of the standard PROLOG interpreter. The graph der ivation can be rebuilt step-by-step and constructively from the resolution- based proof. We provide a notion of CGs in normal form (the table of the co nceptual graph) and show that the PROLOG interpreter also gives a projectio n algorithm between normal CGs, The normal forms are obtained by extending the FOL language by witnesses (new constants) and extending the graph deriv ation system. By applying iteratively a set of rules the reduction process terminates with the normal form of a conceptual graph. We also show that gr aph derivation can be reduced to a question-answering problem in propositio nal datalog for a subclass of simple CGs. The embedding into propositional datalog makes the complexity of the derivation polynomial.