A NEW APPROACH IN AUTOMATED THEOREM PROVING

Award Information
Agency:
National Science Foundation
Amount:
$198,000.00
Program:
SBIR
Contract:
N/A
Solitcitation Year:
N/A
Solicitation Number:
N/A
Branch:
N/A
Award Year:
1988
Phase:
Phase II
Agency Tracking Number:
2621
Solicitation Topic Code:
N/A
Small Business Information
Computer Technology Associates
5670 S Syracuse Cir, Suite 200, Englewood, CO, 80111
Hubzone Owned:
N
Woman Owned:
N
Socially and Economically Disadvantaged:
N
Duns:
N/A
Principal Investigator
 Sidney C Bailin
 Senior Engineer
 (303) 848-2700
Business Contact
Phone: () -
Research Institution
N/A
Abstract
THE PROPOSED RESEARCH AIMS TO EMPLOY A RECENTLY PROVEN GENERALIZATION OF HERBRAND'S THEOREM TO AUTOMATIC THEOREM PROVING (ATP). THE GENERALIZATION, WHICH WAS PROVEN BY THE PRINCIPLE INVESTIGATOR, CHARACTERIZES PROVABILITY IN THE NORMALIZABLE FRAGMENT OF SET THEORY IN TERMS OF PROVABILITY IN PROPOSITIONAL LOGIC. THIS RESULT WILL BE APPLIED TO UTILIZE FINITE MODELS WHICH WILL PROVIDE SEMANTIC GUIDANCE IN THE SEARCH FOR A PROOF. THE MODELS MUST BE FINITE IN ORDER TO BE INCORPORATED IN THESYSTEM. THE HERBRAND-TYPE THEOREM IS REQUIRED TO OBTAIN QUANTIFIER-FREE FORMULAS WHICH CAN BE EVALUATED IN THESE MODELS: ORDINARY FORMULAS OF SET THEORY CONTAIN QUANTIFICATION OVER INFINITE STRUCTURES AND HENCE CAN NOT BEUSED DIRECTLY. THE PROPOSAL IS BASED ON RESEARCH BY THE PRINCIPLE INVESTIGATOR INTO HOW SET THEORY IS PRACTICED BY WORKING MATHEMATICIANS. THE KEY POINT IS THAT EVEN WHEN THE FULL POWER OF SET THEORETIC PRINCIPLES ARE BROUGHT TO BEAR ON A SUBJECT, THE USER OF THESE PRINCIPLES USUALLY HAS A FINITE PICTURE IN MIND WHICH EXEMPLIFIES THE RELATIONS MENTIONED INTHE PROOF. HENCE WE BELIEVE THAT THE PROPOSED APPROACH WILLRESULT IN THE AUTOMATION OF A SIGNIFICANT BODY OF TECHNIQUESWHICH ARE USED IN HUMAN THEOREM PROVING.

* information listed above is at the time of submission.

Agency Micro-sites

US Flag An Official Website of the United States Government