System Description: The Proof Transformation System CERES. - Tsvetan Dunchev; Alexander Leitsch; Tomer Libal; Daniel Weller 001; Bruno Woltzenlogel Paleo (IJCAR, 2010)

A Resolution Calculus for Second-order Logic with Eager Unification. - Alexander Leitsch; Tomer Libal (PAAR@IJCAR, 2012)

Bounded Higher-order Unification using Regular Terms. - Tomer Libal (UNIF, 2012)

System Feature Description: Importing Refutations into the GAPT Framework. - Cvetan Dunchev; Alexander Leitsch; Tomer Libal; Martin Riener; Mikheil Rukhaia; Daniel Weller 001; Bruno Woltzenlogel Paleo (PxTP, 2012)

PROOFTOOL: a GUI for the GAPT Framework. - Cvetan Dunchev; Alexander Leitsch; Tomer Libal; Martin Riener; Mikheil Rukhaia; Daniel Weller 001; Bruno Woltzenlogel Paleo (UITP, 2012)

Understanding Resolution Proofs through Herbrand's Theorem. - Stefan Hetzl; Tomer Libal; Martin Riener; Mikheil Rukhaia (TABLEAUX, 2013)

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. - Damien Doligez; Jael Kriener; Leslie Lamport; Tomer Libal; Stephan Merz (ARQNL@IJCAR, 2014)

Advanced Proof Viewing in ProofTool. - Tomer Libal; Martin Riener; Mikheil Rukhaia (UITP, 2014)

Regular Patterns in Second-Order Unification. - Tomer Libal (CADE, 2015)

Defining the meaning of TPTP formatted proofs. - Roberto Blanco; Tomer Libal; Dale Miller 001 (IWIL@LPAR, 2015)

The Proof Certifier Checkers. - Zakaria Chihani; Tomer Libal; Giselle Reis (TABLEAUX, 2015)

Proving Determinacy of the PharOS Real-Time Operating System. - Selma Azaiez; Damien Doligez; Matthieu Lemerre; Tomer Libal; Stephan Merz (ABZ, 2016)

Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers. - Tomer Libal; Alexander Steen (PAAR@IJCAR, 2016)

Functions-as-Constructors Higher-Order Unification. - Tomer Libal; Dale Miller 001 (FSCD, 2016)

Certification of Prefixed Tableau Proofs for Modal Logic. - Tomer Libal; Marco Volpe 001 (GandALF, 2016)

Determinism in the Certification of UNSAT Proofs. - Tomer Libal; Xaviera Steele (PxTP, 2017)

A Simple Semi-automated Proof Assistant for First-order Modal Logics. - Tomer Libal (ARQNL@IJCAR, 2018)

Automated reasoning in normative detachment structures with ideal conditions. - Tomer Libal; Matteo Pascucci (ICAIL, 2019)

NAI: The Normative Reasoner. - Tomer Libal; Alexander Steen (ICAIL, 2019)

The NAI Suite - Drafting and Reasoning over Legal Texts. - Tomer Libal; Alexander Steen (JURIX, 2019)

A general proof certification framework for modal logic. - Tomer Libal; Marco Volpe 001 (Math. Struct. Comput. Sci., 2019)

A Meta-level Annotation Language for Legal Texts. - Tomer Libal (CLAR, 2020)

Towards an Executable Methodology for the Formalization of Legal Texts. - Tomer Libal; Alexander Steen (CLAR, 2020)

A Bimodal Simulation of Defeasibility in the Normative Domain. - Tomer Libal; Matteo Pascucci; Leon van der Torre; Dov M. Gabbay (FCR@KI, 2020)

Towards Automated GDPR Compliance Checking. - Tomer Libal (TAILOR, 2020)

Towards Transparent Legal Formalization. - Tomer Libal; Tereza Novotná (EXTRAAMAS@AAMAS, 2021)

An Evaluation of Methodologies for Legal Formalization. - Tereza Novotná; Tomer Libal (EXTRAAMAS@AAMAS, 2022)

Do Lawyers Use Automated Reasoning? (invited paper). - Tomer Libal (ARQNL@IJCAR, 2022)

The LegAi Editor: A Tool for the Construction of Legal Knowledge Bases. - Tomer Libal (JURIX, 2022)

Functions-as-constructors higher-order unification: extended pattern unification. - Tomer Libal; Dale Miller 001 (Ann. Math. Artif. Intell., 2022)

Giving Examples Instead of Answering Questions: Introducing Legal Concept-Example Systems. - Tomer Libal; Aleksander Smywinski-Pohl (JURIX, 2023)

Legal linguistic templates and the tension between legal knowledge representation and reasoning. - Tomer Libal (Frontiers Artif. Intell., 2023)

Enhancing Legal Argument Retrieval with Optimized Language Model Techniques. - Aleksander Smywinski-Pohl; Tomer Libal (JSAI-isAI, 2024)

A Legal Assistant for Accountable Decision-Making. - Adam Kaczmarczyk; Tomer Libal; Aleksander Smywinski-Pohl (JURIX, 2024)

Are manual annotations necessary for statutory interpretations retrieval? - Aleksander Smywinski-Pohl; Tomer Libal; Adam Kaczmarczyk; Magdalena Król (CoRR, 2025)