A NEW APPROACH IN AUTOMATED THEOREM PROVING

Award Information
Agency:
National Science Foundation
Branch
n/a
Amount:
$198,000.00
Award Year:
1988
Program:
SBIR
Phase:
Phase II
Contract:
n/a
Award Id:
2621
Agency Tracking Number:
2621
Solicitation Year:
n/a
Solicitation Topic Code:
n/a
Solicitation Number:
n/a
Small Business Information
5670 S Syracuse Cir, Suite 200, Englewood, CO, 80111
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
n/a
Principal Investigator:
Sidney C Bailin
Senior Engineer
(303) 848-2700
Business Contact:
() -
Research Institute:
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


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government