Tomer Libal Technische Universität Wien Favoritenstr. 9-11/E1852 A-1040 Wien, Austria Phone +43-1-58801-18547 Fax +43-1-58801-18597 shaolin [at] logic.at Curriculum vitae

Fields of Interest

• Automated Deduction in Higher-Order Logic.
• Cut Elimination in Higher-Order Proofs.
• Programming.

Published and Submitted Papers

• Alexander Leitsch, Tomer Libal. A Resolution Calculus Based on Eager Second-Order Bounded Unification. Submitted [ pdf ]
• Tomer Libal. Bounded Second-Order Unification Using Regular Terms. Submitted [ pdf ]
• Tomer Libal. Solving Context Related Unification Problems Using Regular Languages. Submitted [ pdf ]
• T. Dunhcev et al. ProofTool: GUI for the GAPT Framework. Submitted [ pdf ]
• T. Dunchev et al. System Feature Description: Importing Refutations into the GAPT Framework. PxTP 2012. Accepted [ pdf ]
• T. Dunchev, A. Leitsch, T. Libal, D. Weller, B. Woltzenlogel Paleo. System Description: The Proof Transformation System CERES, Int. Joint Conference on Automated Reasoning 2010, R. Goebel et al. (eds.), Springer LNCS 6173
• S. Hetzl, A. Leitsch, T. Libal, D. Weller, B. Woltzenlogel Paleo. Resolution Refinements for Cut-Elimination based on Reductive Methods, ESSLLI Workshop on Structures and Deduction (2009) [ pdf ]

Software

• GAPT - Generic Architecture for Proofs

Theses

• Master's Thesis: Cut elimination in inductive proofs of weakly quantified theorems, Vienna University of Technology [ pdf ]