Tomer Libal

Home>Academics>Faculty>Faculty Directory>

Tomer Libal

Assistant Professor

  • Department: Computer Science, Math and Environmental Science
  • Office: 
    PL-1
  • Personal Website: 
    http://tomer.libal.info

See Courses >>

Professor Libal joined The American University of Paris in 2016. His previous positions were in Inria (French Institute for Research in Computer Science and Automation) and Ecole Polytechnique. In 2020, Libal has taken a leave to join the Individual and Collective Reasoning lab in Luxembourg, in order to focus on his work in legal informatics.

After obtaining his BSc in Computer Science and Mathematics from the Hebrew University of Jerusalem in 2001, Libal has spend several years working as a Java team leader for the start-up company Quigo. In 2008 he obtained a double MSc degree in Computational Logic from the technical universities of Madrid, Spain and Vienna, Austria as an Erasmus Mundus scholarship holder. In 2012 he obtained his PhD from the technical university of Vienna with a thesis on Higher-order Automated Deduction.

Libal's research is currently mainly focused on automated legal reasoning and has resulted in publications in various venues (including a best paper award) and software. He has recently received a grant from the Luxembourg National Research Fund for developing further this research.

Previously, Libal's research has focused on BestHigher-order Automated Deduction and especially on variants of higher-order unification. Other topics include Formal Verification and Proof Certification of classic and modal logics. During his professional career, Libal has conducted both theoretical research and implemented tools and software.



Education/Degrees

  • PhD - Technical University of Vienna, Austria (2012)
  • MSc - Technical University of Vienna, Austria (2008)
  • BSc - Hebrew University of Jerusalem, Israel (2001)

News

Publications

  • Tomer Libal, "A Meta-level Annotation Language for Legal Texts Tomer Libal", 2020. CLAR.
  • Tomer Libal and Alexander Steen, "Towards an Executable Methodology for the Formalization of Legal Texts", 2020. CLAR.
  • Tomer Libal, Tereza Novotná, "Towards Automating Inconsistency Checking of Legal Texts", 2020. IRIS.
  • Tomer Libal, Alexander Steen, "NAI - Towards Transparent and Usable Semi-Automated Legal Analysis", 2020. IRIS (best paper award).
  • Tomer Libal, Alexander, "The NAI Suite – Drafting and Reasoning over Legal Texts", 2019. JURIX.
  • Tomer Libal, Matteo Pascucci, "Automated Reasoning in Normative Detachment Structures with Ideal Conditions", 2019. ICAIL.
  • Tomer Libal, Alexander Steen, "NAI – The Normative Reasoner", 2019, ICAIL.
  • Tomer Libal, Marco Volpe, "A general proof certification framework for modal logic", 2019. J. MSCS.
  • Tomer Libal, "A Simple Semi-automated Proof Assistant for First-order Modal Logics", 2018. ARQNL.
  • Tomer Libal, "Implementing a Proof Assistant using Focusing and Logic Programming", 2018, UITP.
  • Tomer Libal, Xaviera Steele, "Determinism in the Certification of UNSAT Proofs", 2017. PxTP
  • T. Libal and M. Volpe, “Certification of prefixed tableau proofs for modal logic,” 2016. GandALF.
  • T. Libal and A. Steen, “Towards a substitution tree based index for higherorder resolution theorem provers,” 2016. PAAR.
  • T. Libal and D. Miller, “Functions-as-constructors higher-order unification,” 2016. FSCD.
  • S. Azaiez, D. Doligez, M. Lemerre, T. Libal, and S. Merz, “Proving determinacy of the pharos real-time operating system,” 2016. ABZ.[5] R. Blanco, T. Libal, and D. Miller, “Defining the meaning of TPTP formatted proofs,” 2015. WIL.
  • T. Libal, “Regular patterns in second-order unification,” 2015. CADE.
  • Z. Chihani, T. Libal, and G. Reis, “The proof certifier checkers,” 2015. TABLEAUX.
  • D. Doligez, J. Kriener, L. Lamport, T. Libal, and S. Merz, “Coalescing: Syntactic abstraction for reasoning in first-order modal logics,” 2015. ARQNL.
  • T. Libal, M. Riener, and M. Rukhaia, “Advanced proof viewing inprooftool,” 2014. UITP.
  • T. Libal, “Bounded higher-order unification using regular terms,” 2014. EPiC Series in Computing.
  • T. Libal, “Utilizing higher-order unifiability algorithms in the resolution calculus,” 2013. ADDCT.
  • S. Hetzl, T. Libal, M. Riener, and M. Rukhaia, “Understanding resolutionproofs through herbrand’s theorem,” 2013. TABLEAUX.
  • C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, and B. W. Paleo, “PROOFTOOL: a GUI for the GAPT framework,” 2013. UITP.
  • A. Leitsch and T. Libal, “A resolution calculus for second-order logic with eager unification,” 2012. PAAR.
  • C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, and B. W. Paleo, “System feature description: Importing refutations into the gapt framework,” 2012. PxTP.
  • T. Dunchev, A. Leitsch, T. Libal, D. Weller, and B. W. Paleo, “System description: The proof transformation system CERES,” 2010. IJCAR.
  • A. L. Stefan Hetzl, T. Libal, D. Weller, and B. W. Paleo, “Resolution refinements for cut-elimination based on reductive methods,” 2009. ESSLI.

Conferences & Lectures

  • Invited tutorial in ReMep 2019.
  • Tutorial in ICAIL 2019.

Affiliations

Association for Automated Reasoning

Research Areas

  • Higher-order Automated Deduction
  • Proof Transformation
  • Proof Certification

Awards, Fellowships and Grants

  • Best paper award in IRIS 2019.
  • Won an FNR PathFinder grant in 2020.

Curriculum Vitae