Variable Elimination and Chaining in a Resolution-based Prover for Inequalities. - W. W. Bledsoe; Larry M. Hines (CADE, 1980)

Hyper-Chaining and Knowledge-Based Theorem Proving. - Larry M. Hines (CADE, 1988)

Str+ve-Subset: The Str+ve-based Subset Prover. - Larry M. Hines (CADE, 1990)

The Central Variable Strategy of Str+ve. - Larry M. Hines (CADE, 1992)

Completeness of a Prover for Dense Linear Orders. - Larry M. Hines (J. Autom. Reason., 1992)

Str+ve and Integers. - Larry M. Hines (CADE, 1994)

Woody Bledsoe - His Life and Legacy. - A. Michael Ballantyne; Robert S. Boyer; Larry M. Hines (AI Mag., 1996)

A Tribute to Woody Bledsoe. - Larry M. Hines (J. Autom. Reason., 1997)