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 decompos ition tree is known. Moreover, the linear-time algorithm can be genera ted automatically from the expression, because all our theorems are pr oved constructively. The calculus is founded upon a short list of part icularly primitive predicates, which in turn are combined by fundament al logical operations. This framework is rich enough to include the va st majority of known linear-time solvable problems. We have obtained t hese results independently of similar results by Courcelle [11], [12], through utilization of the framework of Bern et al. [6]. We believe o ur formalism is more practical for programmers who would implement the automatic generation machinery, and more readily understood by many t heorists.