Incremental Closure of Free Variable Tableaux

Abstract. This paper presents a technique for automated theorem proving with free variable tableaux that does not require backtracking. Most existing automated proof procedures using free variable tableaux require iterative deepening and backtracking over applied instantiations to guarantee completeness. If the correct instantiation is hard to find, this can lead to a significant amount of duplicated work. Incremental Closure is a way of organizing the search for closing instantiations that avoids this inefficiency.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Martin Giese
• Keywords: Applied Instantiations, Automated Reasoning, CADE 2001, Free Variable Tableaux, Iterative Deepening