შოთა რუსთაველის საქართველოს ეროვნული სამეცნიერო ფონდიდაწყების თარიღი: 2013-12-24 დასრულების თარიღი: 2014-12-24
ავტომატური მსჯელობა ლოგიკისა და კომპიუტერულ მეცნიერებათა ერთ-ერთი მნიშვნელოვანი დარგია. ის ასევე განიხილება როგორც ხელოვნური ინტელექტის ქვედარგი. ეს მიმართულება სწავლობს მსჯელობის სხვადასხვა ასპექტებს. ავტომატური მსჯელობის ყველაზე მნიშვნელოვანი ატრიბუტებია კლასიკური პრედიკატთა აღრიცხვა და ლოგიკის სხვადასხვა კალკულუსები.
თეორემათა ავტომატური მტკიცება ავტომატური მსჯელობის ქვედარგია და ამ მიმართულებით ძალიან ბევრი ნაშრომი არსებობს. ერთ-ერთი მნიშვნელოვანი პრობლემა კი თეორემათა მამტკიცებლებისათვის კარგი გრაფიკული ინტერფეისის არქონაა. არსებული მამტკიცებლები არ არიან მომხმარებელზე ორიენტირებულები იმ თვალსაზრისით, რომ მათ გააჩნიათ მხოლოდ ტექსტური ინტერფეისი და ე.წ. “ფლაგები”, რომლითაც მომხმარებელი მანიპულირებს ამ სისტემებზე. დღეისათვის ძალიან აქტუალურია მომხმარებლებისთვის გრაფიკული ინტერფეისის შექმნა და ამ თემაზე საერთაშორისო ფორუმებიც კი ტარდება.
თეორემათა ავტომატური მტკიცება არ აღმოჩნდა საკმარისი საინტერესო მათემატიკური მტკიცებებისათვის, რომლებიც მაგალითად შეიცავენ ინდუქციას. პრობლემა მდგომარეობს იმაში, რომ ინდუქციის წესი ვერ წარმოდგინდება პირველი რიგის ლოგიკაში (მისი ფორმალიზება ხდება მეორე და მაღალი რიგის ლოგიკებში). ის არის ე.წ. მეტა წესი, ან წესის სქემა, რომელიც უსასრულო მოდუს პონენსის წესს შეესაბამება. ამიტომ, პროგრამას მტკიცების ძიებისას ინდუქციის გამოსაყენებლად სჭირდება მომხმარებელთან ინტერაქცია.
რამდენიმე წლის წინ შეიქმნა ინდუქციური სისტემების ალტერნატივა, სახელწოდებით მტკიცებათა სქემები, რომელიც გვერდს უვლის ინდუქციის აქსიომის გამოყენებას. აღნიშნული სქემები დაფუძნებულია პრიმიტიულ-რეკურსულ განსაზღვრებებზე. ფორმულები და დამტკიცებები აგებულია სტანდარტული წესებით, ხოლო შემდეგ მათზე პრიმიტიული რეკურსიით მიღებულია ფორმულათა და მტკიცებათა სქემები.
თეორემათა მტკიცების ტექნიკები იყოფა ორ ნაწილად, მიზანზე მიმართულ და საწინააღმდეგოს უარყოფის მეთოდებად. ამ პროექტის ფარგლებში განვიხილავთ მიზანზე მიმართულ დამტკიცებათა ძებნის ალგორითმს, რომელიც დაფუძნებულია სეკვენციათა კალკულუსზე. სეკვენციათა კალკუსის მთავარი პრობლემა მტკიცებათა ძებნისას არის ის, რომ იგი არადეტერმინირებადი კალკულუსია, რაც ნიშნავს, რომ არ არსებობს გამოყვანის წესების განსაზღვრული რიგითობა, რომელი რომლის შემდეგ უნდა იქნას გამოყენებული. ასეთ თავისუფლებას კი მივყავართ ზედმეტად დიდ ძებნის არემდე. არსებობს ე.წ. ფოკუსირების ტექნიკა, რომელიც გვერდს უვლის არადეტერმინირებულობის თვისებას და მკაცრად განსაზღვრავს წესების რიგითობას. მოცემული პროექტის ფარგლებში ჩვენ შევისწავლით მსგავს ტექნიკას დამტკიცებათა სქემების აგებისას და განვახორციელებთ შესაბამისი ალგორითმების რეალიზაციას.