Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints Mark H. LiffitonKarem A. Sakallah OriginalPaper 13 September 2007 Pages: 1 - 33
Translating Higher-Order Clauses to First-Order Clauses Jia MengLawrence C. Paulson OriginalPaper 15 September 2007 Pages: 35 - 60
On the Mechanization of the Proof of Hessenberg’s Theorem in Coherent Logic Marc BezemDimitri Hendriks OriginalPaper 29 November 2007 Pages: 61 - 85