Author:Tomer Libal

Publications
Defining the meaning of TPTP formatted proofs Roberto Blanco, Tomer Libal and Dale Miller In:IWIL-2015. 11th International Workshop on the Implementation of Logics
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal and Stephan Merz In:ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics
Bounded Higher-order Unification using Regular Terms Tomer Libal In:UNIF 2012 Post-Worskhop Proceedings. The 26th International Workshop on Unification
A Resolution Calculus for Second-order Logic with Eager Unification Alexander Leitsch and Tomer Libal In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning

Keyphrases

Bounded unification², bounded unification algorithms, Decidable unification problems, Dedukti, Efficient second-order theorem proving, Exponent of periodicity, Higher-order resolution, higher-order unification, modal logic, proof certification, proofcert, regular expressions, regular terms, temporal logic, TLA, TPTP, TSTP.