Tomer Libal

Assistant Professor

  • Department: Computer Science Math and Environmental Science
  • Office: 

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.

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.

He is a member of the Association for Automated Reasoning. Libal's research is mainly focused on Higher-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.


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



  • 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.


Association for Automated Reasoning

Research Areas

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

Curriculum Vitae