Skip Navigation

The Computer Journal 2000 43(1):1-12; doi:10.1093/comjnl/43.1.1
© 2000 by British Computer Society
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (7)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Amati, G.
Right arrow Articles by Ounis, I.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Conceptual Graphs and First Order Logic

Gianni Amati1,2 and Iadh Ounis2

1 Fondazione Ugo Bordoni, v. B. Castiglione, 59, 00142 Rome, Italy Email: gba@fub.it 2 Department of Computing Science, University of Glasgow, Glasgow G12 8QQ, UK Email: ounis@dcs.gla.ac.uk

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 interpretation of CGs into first order logic (FOL). The proof is obtained by reducing the graph derivation to a question-answering problem. The graph derivation can be equivalently obtained by querying a Definite Horn Clauses program by a conjunction of positive atoms. Moreover, the proof provides an algorithm for graph derivation in a pure proof-theoretic fashion, namely by means of a slight enhancement of the standard PROLOG interpreter. The graph derivation 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 conceptual graph) and show that the PROLOG interpreter also gives a projection algorithm between normal CGs. The normal forms are obtained by extending the FOL language by witnesses (new constants) and extending the graph derivation system. By applying iteratively a set of rules the reduction process terminates with the normal form of a conceptual graph. We also show that graph derivation can be reduced to a question-answering problem in propositional datalog for a subclass of simple CGs. The embedding into propositional datalog makes the complexity of the derivation polynomial.

Received 7 August, 1998. Revised 4 November, 1999.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.