Publications

To contribute to the web site, please open an issue, create a pull request or send a mail to the science communication coordinators.

STSM reports

• STSM reports

2023

• Benchmarking Local Robustness of High-Accuracy Binary Neural Networks for Enhanced Traffic Sign Recognition, Andreea Postovan and Mădălina Eraşcu, FROM’23

• Terms for Efficient Proof Checking and Parsing, Michael Färber, CPP’23

• Solving Modal Logic Problems by Translation to Higher-order Logic, Alexander Steen, Geoff Sutcliffe, Tobias Scholl, and Christoph Benzmüller, CLAR’23

• Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic, Alexander Steen, Geoff Sutcliffe, Pascal Fontaine, and Jack McKeown, LPAR’23

• An Interactive Interpretation Viewer for Typed First-order Logic, Jack McKeown and Geoff Sutcliffe, FLAIRS’23

• VizAR: Visualization of Automated Reasoning Proofs (System Description), Jan Jakubův and Cezary Kaliszyk, CICM’23

• Combining Higher-Order Logic with Set Theory Formalizations, Cezary Kaliszyk and Karol Pąk, JAR

• Experiments on Infinite Model Finding in SMT Solving, Julian Parsert, Chad Brown, Mikolas Janota, and Cezary Kaliszyk, LPAR’23

• Anti-unification and Generalization: A Survey, David M. Cerna and Temur Kutsia, IJCAI’23

• A modular construction of type theories, Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet, and François Thiré, in LMCS

• Translating proofs from an impredicative type system to a predicative one, T. Felicissimo, F. Blanqui and A. Kumar Barnawal, CSL’23

• Tableaux for Realizability of Safety Specifications, Montserrat Hermo, Paqui Lucio, César Sánchez. Formal Methods 2023, p. 495-513.

• Tableaux and sequent calculi for CTL and ECTL: Satisfiability test with certifying proofs and models, Alex Abuin, Alexander Bolotov, Montserrat Hermo, Paqui Lucio. J. Log. Algebraic Methods Program. 130:100828.

2022

• Theorem Proving for Maude Specifications Using Lean, Rubén Rubio and Adrián Riesco, ICFEM’22

• An Implementation of Set Theory with Pointed Graphs in Dedukti, Valentin Blot, Gilles Dowek and Thomas Traversié, LFMTP’22

• Evolution of Automated Deduction and Dynamic Constructions in Geometry, Pedro Quaresma, Mathematics Education in the Age of Artificial Intelligence, 2022

• Four Geometry Problems to Introduce Automated Deduction in Secondary Schools, Pedro Quaresma, Vanda Santos, ThEdu’21

• Lemmaless Induction in Trace Logic, Ahmed Bhayat, Pamina Georgiou, Clemens Eisenhofer, Laura Kovács, Giles Reger, CICM’22

• The Logic Languages of the TPTP World, Geoff Sutcliffe, Logic Journal of the IGPL, 2022

• Learning Higher-Order Logic Programs From Failures, Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk, IJCAI’22

• Adequate and Computational Encodings in the Logical Framework Dedukti, Thiago Felicissimo, FSCD’22

• Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity, Frédéric Blanqui, FSCD’22

• Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting, Michael Färber, CPP’22

• What Can Formal Systems Do For Mathematics? A Discussion Through The Lens Of Proof Assistants: Some Recent Advances, Angeliki Koutsoukou-Argyraki Q&A with Jeremy Avigad, Jasmin Blanchette, Frédéric Blanqui, Kevin Buzzard, Johan Commelin, Manuel Eberl, Timothy Gowers, Peter Koepke, Assia Mahboubi, Ursula Martin, Lawrence C. Paulson, Special Issue for the 60th Anniversary of the DVMLG (German Association for Mathematical Logic and for Basic Research in the Exact Sciences), Benedikt Löwe, Deniz Sarikaya (eds.), College Publications, 2022

• Vers une traduction de K en Dedukti (Towards a translation of K in Dedukti), Amélie Ledein, Valentin Blot, Catherine Dubois, JFLA’22

• Bécassine à la chasse au Coq, Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial, JFLA’22

Reports

• 2nd WG3 meeting, Timisoara, 8-9 February 2023, slides&videos report

• 1st WG3 meeting, Valencia, 10-11 February 2022 slides&videos report