Tabling for higher-order logic programming

Abstract

We describe the design and implementation of a higher-order tabled logic programming interpreter where some redundant and infinite computation is eliminated by memoizing sub-computation and re-using its result later. In particular, we focus on the table design and table access in the higher-order setting where many common operations are undecidable in general. To achieve a space and time efficient, implementation, we rely on substitution factoring and higher-order substitution tree indexing. Experimental results from a wide range of examples (prepositional theorem proving, refinement type checking, small-step evaluator) demonstrate that higher-order tabled logic programming yields a more robust and more powerful proof procedure. © Springer-Verlag Berlin Heidelberg 2005.