Tomer Libal

Assistant Professor

  • Department: Computer Science Math and Environmental Science
  • Office: 
  • Office Hours: 
    Tuesdays 11:00-12:00

See Courses >>

Professor Libal joined The American University of Paris in 2016 as a lecturer.
He also holds researcher positions in Inria (French Institite 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 was among the first to join the start-up company Quigo.
In his role as a team leader, Libal has managed the company's Data Mining and Extraction division from its head quarters in New York city.
The company was sold to AOL in 2007 for $360M.

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.

Since 2012, Libal has worked as a post-doctoral researcher in research centers of Inria, MSR (Microsoft Research) and Ecole Polytechnique.
He is a member of the Association for Automated Reasoning.

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

In 2016, Libal has presented his research at FSCD, Porto; PAAR, Coimbra and GandALF, Catania.


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



[1]T. Libal and M. Volpe, “Certification of prefixed tableau proofs for modal
logic,” 2016. GandALF.
[2] T. Libal and A. Steen, “Towards a substitution tree based index for higher-
order resolution theorem provers,” 2016. PAAR.
[3] T. Libal and D. Miller, “Functions-as-constructors higher-order unifica-
tion,” 2016. FSCD.
[4] S. Azaiez, D. Doligez, M. Lemerre, T. Libal, and S. Merz, “Proving deter-
minacy of the pharos real-time operating system,” 2016. ABZ.
[5] R. Blanco, T. Libal, and D. Miller, “Defining the meaning of TPTP for-
matted proofs,” 2015. IWIL.
[6] T. Libal, “Regular patterns in second-order unification,” 2015. CADE.
[7] Z. Chihani, T. Libal, and G. Reis, “The proof certifier checkers,” 2015.
[8] D. Doligez, J. Kriener, L. Lamport, T. Libal, and S. Merz, “Coalescing:
Syntactic abstraction for reasoning in first-order modal logics,” 2015. AR-
[9] T. Libal, M. Riener, and M. Rukhaia, “Advanced proof viewing in
prooftool,” 2014. UITP.
[10] T. Libal, “Bounded higher-order unification using regular terms,” 2014.
EPiC Series in Computing.
[11] T. Libal, “Utilizing higher-order unifiability algorithms in the resolution
calculus,” 2013. ADDCT.
[12] S. Hetzl, T. Libal, M. Riener, and M. Rukhaia, “Understanding resolution
proofs through herbrand’s theorem,” 2013. TABLEAUX.
[13] C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, and
B. W. Paleo, “PROOFTOOL: a GUI for the GAPT framework,” 2013.
[14] A. Leitsch and T. Libal, “A resolution calculus for second-order logic with
eager unification,” 2012. PAAR.
[15] 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.
[16] T. Dunchev, A. Leitsch, T. Libal, D. Weller, and B. W. Paleo, “System
description: The proof transformation system CERES,” 2010. IJCAR.
[17] 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