Deductive synthesis of sorting programsJournal of Symbolic Computation, June 1989
https://www.sciencedirect.com/science/article/pii/S0747717189800409
Nested Resolution, Procedings of CADE 8 https://cadeinc.org/
https://en.wikipedia.org/wiki/Resolution_(logic)#Non-clausal_resolution
Advising: N/A
