A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry Gabriel BraunJulien Narboux OriginalPaper 29 April 2016 Pages: 209 - 230
Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System Ana Cristina Rocha-OliveiraAndré Luiz GaldinoMauricio Ayala-Rincón OriginalPaper 07 June 2016 Pages: 231 - 251
A Fully Automatic Theorem Prover with Human-Style Output M. GanesalingamW. T. Gowers OriginalPaper Open access 11 June 2016 Pages: 253 - 291
Higher-Order Pattern Anti-Unification in Linear Time Alexander BaumgartnerTemur KutsiaMateu Villaret OriginalPaper Open access 27 July 2016 Pages: 293 - 310