Artículos de revistas
Using Difference Reduction for Generic Proof Search
Autor
NEGRETE , SANTIAGO
Institución
Resumen
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. 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.