info@viam.science.tsu.ge (+995 32) 2 30 30 40 (+995 32) 2 18 66 45

Automated and Interactive Theorem Proving in Schemata and Unranked Logics (FR/51/4-102/13)


Funded by

SRNSFGShota Rustaveli National Science Foundation of Georgia

Start Date: 2014-04-02       End Date: 2017-04-02

Automated reasoning is one of the most important research area in logic and computer science. It is also considered as a sub-field of artificial intelligence. It studies different aspects of reasoning. The most important tools of automated reasoning are different calculi for classical logic.

The main two sub-fields of automated reasoning are the fields of automated and interactive theorem proving. The research subjects of this project are exactly these directions. More specifically, we have studied automated reasoning methods for schematic and unranked logics.

The achieved results are both of theoretical and practical character. We have constructed new solving procedures for schemata and unranked logics and improved proof representation formats for them. All the algorithms and procedures developed in the project was implemented and are available for practical usage.

Theoretical significance of the achieved results for scientific directions can be considered in two aspects. The first aspect in this case is significance for the development and extension of the fields of schemata and unranked logics by bringing in new calculi and algorithms to reason on them.

The second aspect is related to applications in the other fields. In this respect, the results of the project expand existing and create new techniques in automated and interactive theorem proving. A user friendly graphical user interface, together with the theorem provers on new kind of logics, potentially are enlarging usage area and increasing number of users for this kind of programs. Our results can be applied in the areas such as semantic web and knowledge representation.

Project members:

Talks

  • Constraint Logic Programming for Hedges: aSemantic Reconstruction, by Besik Dundua (Speaker), Mario Florido, Temur Kutsia, Mircea Marin at International Symposium on Functional and Logic Programming, 2014, Kanazawa, Japan .
  • About Correspondence Between Proof Schemata and Unranked Logics, by Lia Kurtanidze (Speaker), Gela Chankvetadze, Mikheil Rukhaia at VI Annual International Conference of the Georgian Mathematical Union, 2015, Batumi, Georgia.
  • Semi-Automated Construction of Proof Schemata, by Mikheil Rukhaia (Speaker), Gela Chankvetadze, Lia Kurtanidze at Eleventh International Tbilisi Symposium on Language, Logic and Computation, 2015, Tbilisi, Georgia.
  • Theorem Proving in Formula Schemata, by Mikheil Rukhaia (Speaker) at Fourth International Workshop on Proof Exchange for Theorem Proving, 2015, Berlin, Germany.
  • Prover for Unranked Propositional Logic, by Mikheil Rukhaia (Speaker), Gela Chankvetadze at Application of Mathematics and Informatics in Natural Sciences and Engineering, 2015, Tbilisi, Georgia.
  • Automated Theorem Prover for Unranked Logics, by Mikheil Rukhaia (Speaker), Gela Chankvetadze, Lia Kurtanidze at VII International Joint Conference of the Georgian Mathematical Union and the Georgian Mechanical Union Dedicated to 125-th Birthday Anniversary of Academician N. Muskhelishvili, 2016, Batumi, Georgia.
  • Inductive Theorem Proving with Schemata, by Mikheil Rukhaia (Speaker) at First Erasmus+ International Credit Mobility Conference and Workshops, 2016, Braganca, Portugal.
  • Proof Consturction in First-Order Unranked Logic, by Mikheil Rukhaia (Speaker), Gela Chankvetadze at XXX International Enlarged Sessions of the Seminar of Ilia Vekua Institute of Applied Mathematics, 2016, Tbilisi, Georgia.
  • Solving Hedge Regular and Context Regular Inequalities, by Besik Dundua (Speaker) at Oberseminarder Theorie, 2017, Stuttgart, Germany.
  • An Overview of PρLog , by Besik Dundua (Speaker), Temur Kutsia, Klaus Reisenberger-Hagmayer at International Symposium on Practical Aspects of Declarative Languages, 2017, Paris,France .
  • Unranked Tableaux Calculus for Web Related Applications, by Besik Dundua (Speaker), Mikheil Rukhaia, Lia Kurtanidze at IEEE First Ukraine Conferenceon Electrical and Computer Engineering, 2017, Kiev, Ukraine .
  • Tableaux Calculus for Unranked Logics, by Lia Kurtanidze (Speaker), Mikheil Rukhaia at Students and Young Scientists Conference on Science and Modern Technologies, 2017, Tskaltubo, Georgia.
  • Tableaux Calculus for Unranked Logics, by Lia Kurtanidze (Speaker), Mikheil Rukhaia at Twelfth International Tbilisi Symposium on Language, Logic and Computation, 2017, Lagodekhi, Georgia.

Publications

  • Lia Kurtanidze, Mikheil Rukhaia, About Correspondence Between Proof Schemata and Unranked Logics, In: Jangveladze, Temur and Kiguradze, Zurab (eds.): Reports of Enlarged Sessions of the Seminar of I. Vekua Institute of Applied Mathematics, vol. 29. pp. 72–75, Tbilisi University Press, 2015.
  • Gela Chankvetadze, Lia Kurtanidze, Mikheil Rukhaia, Semi-Automated Construction of Proof Schemata, In: Journal of Applied Mathematics, Informatics and Mechanics, vol. 21 (2), pp. 83–91, Tbilisi University Press, 2016.
  • Gela Chankvetadze, Lia Kurtanidze, Mikheil Rukhaia, Proof Construction in Unranked Logic, In: Jangveladze, Temur and Kiguradze, Zurab (eds.): Reports of Enlarged Sessions of the Seminar of I. Vekua Institute of Applied Mathematics, vol. 30. pp. 11–14, Tbilisi University Press, 2016.
  • Besik Dundua, Lia Kurtanidze, Mikheil Rukhaia, Unranked Tableaux Calculus for Web Related Applications, In IEEE First Ukraine Conference on Electrical and Computer Engineering, pp. 1181-1184, IEEE, 2017.

Additional Information

During the project we have developed two provers: