Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints
Translating Higher-Order Clauses to First-Order Clauses
On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic