A NEW APPROACH IN AUTOMATED THEOREM PROVING

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.