Using Difference Reduction for Generic Proof Search
Santiago Negrete · LA Referencia (Red Federada de Repositorios Institucionales de Publicaciones Científicas) · 1998
IN THIS PAPER A NEW APROACH TO GENERIC THEOREM PROVING IS INTRODUCED. WE PRESENT A SET OF TECHNIQUES TO GUIDE PROOF SEARCH IN FRAMEWORK THEORIES THAT WORKS WITH DIFFERENT OBJECT THEORIES ENCODED. THE TECHNIQUES ARE BASED ON THE PRICIPLE OF DIFFERENCE REDUCTION AND PROGRAMMED IN A PROOF PLANS ENVIROMENT. WE USE PRESENTATIONS OF LOGIES IN NATURAL DEDUCTION STYLE TO TEST OUR TECHNIQUES TWO EXAMPLE THEOREM PROOFS ARE INCLUDED TO SHOW HOW THE WHOLE SETTING WORKS.