Theorem proving with abstraction, part II /

Supported in part by the National Science Foundation under grant MCS 77-22830.

Theorem proving with abstraction, part I /

"UILU-ENG 79-1706."

Some new results on resolution in automated theorem proving,

Issued also as thesis (M.S.) University of Illinois.

A recursively defined ordering for proving termination of term rewriting systems /

NSF MCS 77-22830."

A resolution style proof procedure for higher-order logic /

Thesis--Illinois.

A note on simplification orderings /

"April 1979."