You are here

A NEW APPROACH IN AUTOMATED THEOREM PROVING

Award Information
Agency: National Science Foundation
Branch: N/A
Contract: N/A
Agency Tracking Number: 2621
Amount: $198,000.00
Phase: Phase II
Program: SBIR
Solicitation Topic Code: N/A
Solicitation Number: N/A
Timeline
Solicitation Year: N/A
Award Year: 1988
Award Start Date (Proposal Award Date): N/A
Award End Date (Contract End Date): N/A
Small Business Information
5670 S Syracuse Cir Suite 200
Englewood, CO 80111
United States
DUNS: N/A
HUBZone Owned: No
Woman Owned: No
Socially and Economically Disadvantaged: No
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. *

US Flag An Official Website of the United States Government