Decomposition techniques and their applications in automated theorem proving
Erica Melis⋆ · 1995
This paper addresses the decomposition of proofs as a means of constructing methods in plan-based automated theorem proving. It shows also, how decomposition can beneficially be applied in theorem proving by analogy. Decomposition is also useful for human-style proof presentation. We propose several decomposition techniques that were found to be useful in automated theorem proving and give examples of their application. 1 Introduction The way human experts solve problems often differs from the way computers solve the same problem. For instance, among other differences, human experts can take larger steps 8 , while automated systems perform well-defined basic steps towards a solution. This is particularly the case in automated theorem proving systems. These systems usually apply fixed proof calculus rules, e.g., resolution, as basic steps. However, some automated theorem provers have in-built procedures that are specialized to deal with particular subproblems 3 ; 15 , and some em...