Combine algebraic theories then attempt to show they are inconsistent.
- From algebraic theories S, T, and variables construct the small composite terms of the from ST
- Construct all small substitutions
- Find all terms of the form ST that reduce to a term of the form TS under substitution
- This then forms potential evidence against the existence of a composite theory U
Based on the work of Dan Marsden and Maaike Zwart, available on the arXiv.