| 2025 | ICAIL | Are manual annotations necessary for statutory interpretations retrieval? | Tomer Libal, Aleksander Smywinski-Pohl, Adam Kaczmarczyk, Magdalena Krl |
| 2024 | JURIX | A Legal Assistant for Accountable Decision-Making. | Adam Kaczmarczyk, Tomer Libal, Aleksander Smywinski-Pohl |
| 2023 | JURIX | Giving Examples Instead of Answering Questions: Introducing Legal Concept-Example Systems. | Tomer Libal, Aleksander Smywinski-Pohl |
| 2022 | CADE | Do Lawyers Use Automated Reasoning? (invited paper). | Tomer Libal |
| 2022 | JURIX | The LegAi Editor: A Tool for the Construction of Legal Knowledge Bases. | Tomer Libal |
| 2020 | KI | A Bimodal Simulation of Defeasibility in the Normative Domain. | Tomer Libal, Matteo Pascucci, Leon van der Torre, Dov M. Gabbay |
| 2019 | ICAIL | Automated reasoning in normative detachment structures with ideal conditions. | Tomer Libal, Matteo Pascucci |
| 2019 | ICAIL | NAI: The Normative Reasoner. | Tomer Libal, Alexander Steen |
| 2019 | JURIX | The NAI Suite - Drafting and Reasoning over Legal Texts. | Tomer Libal, Alexander Steen |
| 2018 | CADE | A Simple Semi-automated Proof Assistant for First-order Modal Logics. | Tomer Libal |
| 2016 | CADE | Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers. | Tomer Libal, Alexander Steen |
| 2015 | CADE | Regular Patterns in Second-Order Unification. | Tomer Libal |
| 2015 | LPAR | Defining the meaning of TPTP formatted proofs. | Roberto Blanco, Tomer Libal, Dale Miller |
| 2015 | TABLEAUX | The Proof Certifier Checkers. | Zakaria Chihani, Tomer Libal, Giselle Reis |
| 2014 | CADE | Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. | Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz |
| 2013 | TABLEAUX | Understanding Resolution Proofs through Herbrand's Theorem. | Stefan Hetzl, Tomer Libal, Martin Riener, Mikheil Rukhaia |
| 2012 | CADE | A Resolution Calculus for Second-order Logic with Eager Unification. | Alexander Leitsch, Tomer Libal |
| 2012 | CADE | Bounded Higher-order Unification using Regular Terms. | Tomer Libal |
| 2010 | CADE | System Description: The Proof Transformation System CERES. | Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo |