This award will support collaborative research between Prof. Jieh Hsiang of the State University of New York at Stony Brook, and Prof. Jean-Pierre Jouannaud, University of Paris-Sud, Centre d'Orsay, in the area of automated theorem proving. The objective of this work is to investigate in an efficient manner the usefulness of a large number of theorem-proving strategies developed by these investigators. The researchers are most involved with strategies involving equality and deletion inference rules, which are utilized most efficiently in derivations based upon refutational strategies. They will develop a framework for expressing refutational strategies. Using this framework as well as a new proof technique which has been successful in proving the completeness of a wide variety of theorem proving methods, they will begin development of a uniform programming environment for producing and experimenting with computerized theorem provers. The French collaborator has considerable experience in the field of artificial intelligence and automated theorem proving. Cooperative research with the U.S. investigator dates to 1983, involving exchanges of individuals from both laboratories and has resulted in considerable progress in the areas to be extended by the current work. The research results could have a significant impact on the future design and implementation of theorem provers and proof checkers, and on the theoretical basis of artificial intelligence itself.
