U.S.-France Cooperative Research: Studies in the Theory and Implementation of Automated Theorem Provers
{'Code': '01090000', 'Directorate': {'Abbreviation': 'O/D', 'LongName': 'Office Of The Director'}, 'Division': {'Abbreviation': 'OISE', 'LongName': 'Office Of Internatl Science &Engineering'}}
{'SignBlockName': 'Pierre Perrolle', 'PO_EMAI': None, 'PO_PHON': None}
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.
{'FirstName': 'Jieh', 'LastName': 'Hsiang', 'PI_MID_INIT': None, 'PI_SUFX_NAME': None, 'PI_FULL_NAME': 'Jieh Hsiang', 'EmailAddress': 'hsiang@sbcs.sunysb.edu', 'NSF_ID': '000182515', 'StartDate': '01/01/1988', 'EndDate': None, 'RoleCode': 'Principal Investigator'}
{'Name': 'SUNY at Stony Brook', 'CityName': 'STONY BROOK', 'ZipCode': '117940001', 'PhoneNumber': '6316329949', 'StreetAddress': 'W5510 FRANKS MELVILLE MEMORIAL L', 'StreetAddress2': None, 'CountryName': 'United States', 'StateName': 'New York', 'StateCode': 'NY', 'CONGRESSDISTRICT': '01', 'CONGRESS_DISTRICT_ORG': 'NY01', 'ORG_UEI_NUM': 'M746VC6XMNH9', 'ORG_LGL_BUS_NAME': 'THE RESEARCH FOUNDATION FOR THE STATE UNIVERSITY OF NEW YORK', 'ORG_PRNT_UEI_NUM': None}
{'Name': None, 'CityName': None, 'StateCode': None, 'ZipCode': None, 'StreetAddress': None, 'CountryCode': None, 'CountryName': None, 'StateName': None, 'CountryFlag': None, 'CONGRESSDISTRICT': None, 'CONGRESS_DISTRICT_PERF': '""'}
{'Code': '5918', 'Text': 'FRANCE'}
{'url': 'https://www.nsf.gov/awardsearch/download?DownloadFileName=1987&All=true', 'xml': '8715231.xml'}