Dr. John
E. Heaton
Brief Biography and Contact Details
John E. Heaton received his doctorate from Loughborough University of Technology in 1995 having previously gained an MSc during which he was introduced to Conceptual Graphs. His Doctoral thesis, Goal Driven Theorem Proving Using Conceptual Graphs And Peirce Logic, analysed John Sowa's theory of Conceptual Graphs, expanded the theory, resolved a number of ambiguities and took from this the essential elements for the building of sophisticated theorem provers.
In particular Dr. Heaton developed methods of proof that removed the restrictions imposed by traditional rule-based or resolution based approaches. He developed proof strategies which employed the open world assumptions (three truth values – true, false and unknown – and arbitrary negation) instead of the more usual closed world assumptions (two truth values – true and false – and no arbitrary negation). This allowed his theorem provers great expressive power.
Following his doctoral work Dr. Heaton has taken his theory much further. He has developed and implemented a resolution-like proof technique specifically for the open world assumptions. Computational complexity is a problem with very expressive systems but Dr. Heaton's discovery of a set rules which govern the selection of which branches of a proof tree can be shown to be unfruitful and therefore ignored lead to massive increases in efficiency.
Dr. Heaton's theory is embodied in his Prolog implementation known as OWLS (Open World Logic System). This is a prototype system which demonstrates the theory and which was presented at the International Conference on Conceptual Structures in Darmstadt in 2000 (ICCS2000). There are also papers included in the proceedings of the 1990 Workshop on Conceptual Graphs and the International Conference On Conceptual Structures 2000 (ICCS).