USA flag logo/image

An Official Website of the United States Government

A NEW APPROACH IN AUTOMATED THEOREM PROVING

Award Information

Agency:
National Science Foundation
Branch:
N/A
Award ID:
2621
Program Year/Program:
1988 / SBIR
Agency Tracking Number:
2621
Solicitation Year:
N/A
Solicitation Topic Code:
N/A
Solicitation Number:
N/A
Small Business Information
Computer Technology Associates
5670 S Syracuse Cir Suite 200 Englewood, CO 80111
View profile »
Woman-Owned: No
Minority-Owned: Yes
HUBZone-Owned: No
 
Phase 2
Fiscal Year: 1988
Title: A NEW APPROACH IN AUTOMATED THEOREM PROVING
Agency: NSF
Contract: N/A
Award Amount: $198,000.00
 

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.

Principal Investigator:

Sidney C Bailin
Senior Engineer
3038482700

Business Contact:

Small Business Information at Submission:

Computer Technology Associates
5670 S Syracuse Cir Suite 200 Englewood, CO 80111

EIN/Tax ID:
DUNS: N/A
Number of Employees: N/A
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No