Mikheil Rukhaia

Researcher
Institute of Applied Mathematics,
Tbilisi State University.

E-mail:	mrukhaia [at] logic.at
Address:	University str. 2, VIAM, 0186 Tbilisi, Georgia

For more information about me see my Curriculum Vitae.

Projects

• STRUCTURAL: Structural and Computational Proof Theory.
• ASAP: About Schemata And Proofs.
• GAPT: General Architecture for Proof Theory.

Talks

2013

• A Method Overcoming Induction During Cut-Elimination, Tenth International Tbilisi Symposium on Language, Logic and Computation, Gudauri, Georgia. [slides]

2012

• CERES in Proof Schemata, PhD Defence, Vienna University of Technology, Vienna, Austria. [slides]
• ProofTool: GUI for the GAPT Framework, 10th International Workshop On User Interfaces for Theorem Provers, Bremen, Germany. [slides]
• CERES for Propositional Proof Schemata (refined version), ASAP Project Meeting, Grenoble, France. [slides]

2011

• CERES for Propositional Proof Schemata, Workshop on Structural and Computational Proof Theory, Innsbruck, Austria. [slides]
• CERES and Fast Cut-Elimination, Ninth International Tbilisi Symposium on Language, Logic and Computation, Kutaisi, Georgia. [slides]

2009

• Second Order Cut-Elimination, Eighth International Tbilisi Symposium on Language, Logic and Computation, Bakuriani, Georgia. [slides]

2006

• მოდელირება მათემატიკური ლოგიკის ენაზე (Modeling on Mathematical Logic Language), Post and Undergraduate Students 66 Conference, Tbilisi State University, Tbilisi, Georgia.

Publications

2014

• T. Libal, M. Riener, M. Rukhaia, Advanced Proof Viewing in ProofTool. In Proceedings of 11th International Workshop On User Interfaces for Theorem Provers (UITP 2014). [online]

2013

• S. Hetzl, T. Libal, M. Riener, M. Rukhaia, Understanding Resolution Proofs through Herbrand's Theorem. In Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2013). [online]

PhD Thesis

CERES in Proof Schemata, Vienna University of Technology, 2012. [pdf]
A revised version, About Cut-Elimination in Schematic Proofs, is published by Lambert Academic Publishing as a monograph in 2013. [poster] [online]

2012

• C. Dunchev, A. Leitsch, M. Rukhaia, D. Weller, CERES for First-Order Schemata. Technical Report, Vienna University of Technology. [online]
• C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel-Paleo, ProofTool: a GUI for the GAPT Framework. In Proceedings of 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012). [online]
• C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia, D. Weller, B. Woltzenlogel-Paleo, System Feature Description: Importing Refutations into the GAPT Framework. In Proceedings of Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012). [online]
• C. Dunchev, A. Leitsch, M. Rukhaia, D. Weller, CERES for Propositional Proof Schemata. Technical Report, Vienna University of Technology. [paper]

Masters Thesis

CERES and Fast Cut-Elimination, Vienna University of Technology, 2009. [poster]
A revised version is published by VDM Verlag Dr. Müller as a monograph in 2011. [online]

2009

• M. Rukhaia, Implementation of Second Order Cut-Elimination. Technical Report, Vienna University of Technology. [paper]
• M. Rukhaia, Integration of Ontologies with Rule Systems (a survey). In Reports of Enlarged Sessions of the Seminar of I. Vekua Institute of Applied Mathematics, volume 23, Tbilisi, Georgia. [online]