A direct proof procedure for definite conceptual graph programs

Abstract

Conceptual graphs form the basis of a graph-based existential-conjunctive logic. In this paper, first, we illustrate the problems associated with a proof procedure for conceptual graph programs and then specify the definitions of a normal form representation for a conceptual graph program, an anti-normal form representation for a goal, and a conceptual graph unification procedure called CG unification. Next, we develop a direct proof procedure for definite conceptual graph programs, called CGF-derivation. The proof procedure takes advantage of the normal form of a definite conceptual graph program and the anti-normal form of a goal, and utilizes the CG unification procedure for matching conceptual graphs. Finally, we prove that the proposed CGF-derivation procedure is sound and complete.