| საქართველოს ეროვნული სამეცნიერო ფონდის პროექტი |
VIAMVIAM SeminarEnlarged Sessions of the VIAM SeminarScientific ProjectsShota Rustaveli National Science Foundation's Projects NATO Science Programme (Collaborative Linkage Grant NATO PST.CLG.976426/5437) TICMIGeoMechUnionStatute of the Georgian Mechanical Union Georgian National Committee of Theoretical and Applied Mechanics GNSTAMConferences |
თეორემათა ავტომატური და ინტერაქციული მტკიცება სქემებსა და ურანგო ლოგიკაშიშოთა რუსთაველის ეროვნული სამეცნიერო ფონდის საგრანტო პროექტი ფუნდამენტური კვლევებისათვის № FR/51/4-102/13სამეცნიერო ხელმძღვანელი: მიხეილ რუხაიაპროექტის რეზიუმეავტომატური მსჯელობა ლოგიკისა და კომპიუტერულ მეცნიერებათა ერთ-ერთი ყველაზე მნიშვნელოვანი დარგია. ის ასევე განიხილება როგორც ხელოვნური ინტელექტის ქვედარგი. ეს მიმართულება სწავლობს მსჯელობის სხვადასხვა ასპექტებს. ავტომატური მსჯელობის ყველაზე მნიშვნელოვანი ატრიბუტებია კლასიკური პრედიკატთა აღრიცხვა და ლოგიკის სხვადასხვა კალკულუსები. ავტომატური მსჯელობის ორი ძირითადი ქვედარგია თეორემათა ავტომატური და ინტერაქციული მტკიცებები. აღნიშნული პროექტის კვლევის ობიექტიც სწორედ ეს მიმართულებებია. უფრო კონკრეტულად, ჩვენ შევისწავლეთ სქემებისა და ურანგო ლოგიკისათვის ავტომატური მსჯელობის მეთოდები. მიღებული შედეგები როგორც თეორიული, ისე პრაქტიკული ხასიათისაა. ჩვენ ავაგეთ ამოხსნის ახალი პროცედურები სქემებისა და ურანგო ლოგიკისათვის და გავაუმჯობესეთ მათი დამტკიცებათა წარმოდგენის ფორმატები. პროექტის მიმდინარეობისას შექმნილი ყველა ალგორითმი და პროცედურა იქნა რეალიზებული და შესაძლებელია მათი პრაქტიკაში გამოყენება. მიღებული შედეგების თეორიული მნიშვნელობა მეცნიერული დარგების მიმართ შესაძლებელია განვიხილოთ ორ ასპექტში. პირველი ასპექტი ჩვენს შემთხვევაში გულისხმობს სქემებისა და ურანგო ლოგიკის მიმართულებების განვითარებასა და გაფართოებას ახალი კალკულუსებისა და მათზე მსჯელობის ალგორითმების შემოღებით. მეორე ასპექტი მიღებული შედეგების სხვა სფეროებში გამოყენებას უკავშირდება. ამ მხრივ, პროექტის შედეგები განავრცობენ არსებულს და ქმნიან ახალ ტექნოლოგიებს თეორემათა ავტომატურ და ინტერაქციულ მტკიცებაში. მომხმარებელზე ორიენტირებული გრაფიკული ინტერფეისი, ახალი ტიპის ლოგიკებისათვის თეორემათა დამამტკიცებლებთან ერთად, პოტენციურად აფართოებს ამ ტიპის პროგრამების მომხმარებელთა არეს და ზრდის მათ რიცხვს. ჩვენს მიერ მიღებული შედეგები შესაძლებელია გამოყენებულ იქნას ისეთ დარგებში, როგორიცაა სემანტიკური ქსელი და ცოდნის წარმოდგენა. პროგრამული პროდუქტიპროექტის ფარგლებში შემუშავდა ორი პროგრამული პროდუქტი:
Automated and Interactive Theorem Proving in Schemata and Unranked LogicsShota Rustaveli National Science Foundation Grant for Fundamental Research № FR/51/4-102/13Principal Investigator: Mikheil RukhaiaProject AbstractAutomated 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. ProductsDuring the project we have developed two provers:
|