AUTOMATIC-GENERATION OF LINEAR-TIME ALGORITHMS FROM PREDICATE CALCULUS DESCRIPTIONS OF PROBLEMS ON RECURSIVELY CONSTRUCTED GRAPH FAMILIES

This paper describes a predicate calculus in which graph problems can be expressed. Any problem possessing such an expression can be solved in linear time on any recursively constructed graph, once its decomposition tree is known. Moreover, the linear-time algorithm can be generated automatically from the expression, because all our theorems are proved constructively. The calculus is founded upon a short list of particularly primitive predicates, which in turn are combined by fundamental logical operations. This framework is rich enough to include the vast majority of known linear-time solvable problems. We have obtained these results independently of similar results by Courcelle [11], [12], through utilization of the framework of Bern et al. [6]. We believe our formalism is more practical for programmers who would implement the automatic generation machinery, and more readily understood by many theorists.