Boolean Reasoning in a Higher-Order Superposition Prover. - Petar Vukmirovic; Visa Nummelin (PAAR+SC²@IJCAR, 2020)

Superposition with First-class Booleans and Inprocessing Clausification. - Visa Nummelin; Alexander Bentkamp; Sophie Tourret; Petar Vukmirovic (CADE, 2021)

Efficient Full Higher-Order Unification. - Petar Vukmirovic; Alexander Bentkamp; Visa Nummelin (Log. Methods Comput. Sci., 2021)

Making Higher-Order Superposition Work. - Petar Vukmirovic; Alexander Bentkamp; Jasmin Blanchette; Simon Cruanes; Visa Nummelin; Sophie Tourret (J. Autom. Reason., 2022)

Recurrence-Driven Summations in Automated Deduction. - Visa Nummelin; Jasmin Blanchette; Sander R. Dahmen (FroCoS, 2023)

Mechanical Mathematicians. - Alexander Bentkamp; Jasmin Blanchette; Visa Nummelin; Sophie Tourret; Petar Vukmirovic; Uwe Waldmann (Commun. ACM, 2023)

Complete and Efficient Higher-Order Reasoning via Lambda-Superposition. - Alexander Bentkamp; Jasmin Blanchette; Visa Nummelin; Sophie Tourret; Uwe Waldmann (ACM SIGLOG News, 2023)