[3][4] Waldinger collaborated with Cordell Green, Robert Yates, Jeff Rulifson, and Jan Derksen on QA4, a PLANNER-like artificial intelligence language geared towards automatic planning and theorem proving.
[5] QA4 introduced the notion of context and also of associative-commutative unification, which made the associative and commutative axioms for operators not only unnecessary but also inexpressible.
In a separate paper, they synthesized a novel square-root algorithm; they found that the notion of binary search appears spontaneously by a single application of the resolution rule to the specification of the square root.
The SNARK system has been incorporated by the Kestrel Institute into their software development environment Specware, which has been used by Waldinger for the validation of the first-order axiomatization of DAML, the DARPA agent markup language, and its successor, OWL.
Recently, Waldinger has worked on the application of deductive methods to answer questions in geography, biology, and intelligence analysis.