Using Difference Reduction for Generic Proof Search

Abstract

Abstract. In this paper a new approach to generic theorem proving is introduced. We present a set 01 techniques to guide prool search in framework theories that works with different object theories encoded. The techniques are based on the principIe 01 Difference Reduction and programmed in a Proof Plans environment. We use presentations ollogics in natural deduction style to test our techniques. Two example theorem prools are included to show how the whole setting works.