შოთა რუსთაველის საქართველოს ეროვნული სამეცნიერო ფონდიდაწყების თარიღი: 2012-03-20 დასრულების თარიღი: 2015-03-20
პროექტის მიზანია გადაწყვეტადობის და ამოხსნის პროცედურების აგება შეზღუდვებისთვის ურანგო ტერმებსა და მათ მიმდევრობებზე და ამ პროცედურების ჩართვა შეზღუდვებიანი ლოგიკური პროგრამირების ზოგად ჩარჩოში.
ურანგო ტერმები ურანგო ფუნქციონალური სიმბოლოების მეშვეობით აიგება. ამ სიმბოლოებს არ აქვთ ფიქსირებული ადგილიანობა. ეს ნიშნავს, რომ ტერმში ერთი და იმავე სიმბოლოს სხვადასხვა შემოსვლას შეიძლება არგუმენტების სხვადასხვა რაოდენობა ჰქონდეს.
ურანგო ფუნქციონალური სიმბოლოების გარდა, ტერმები შეიძლება შეიცავდნენ პირველი და მეორე რიგის ცვლადებს. პირველი რიგის
ცვლადებია ტერმების და მიმდევრობების ცვლადები. მეორე რიგის ცვლადებია ფუნქციონალური და კონტექსტების ცვლადები. ჩასმები
ცვლადებს შესაბამის სტრუქტურებზე ასახავენ: ტერმების ცვლადი აისახება ერთ ტერმზე, მიმდევრობის ცვლადი -- მიმდევრობის ცვლადების და ტერმების მიმდევრობაზე, ფუნქციონალური ცვლადი -- ფუნქციონალურ ცვლადზე ან სიმბოლოზე, კონტექსტის ცვლადი კონტექსტზე. ეს უკანასკნელი ტერმია, რომელშიც სპეციალური სიმბოლო, სახელად ხვრელი, მხოლოდ ერთხელ შემოდის.
ურანგო ტერმები და მათი მიმდევრობები ბოლო წლებში პოპულარული გახდა მათი გამოყენების საინტერესო სფეროების გამო: ისინი მოდელირებას უკეთებენ XML მონაცემებს და დოკუმენტებს, პროგრამების სქემებს, ამბიენტებს, მრავალარხიანი რეკურსიული პროგრამების კონფიგურაციებს შემოუსაზღვრელი პარალელური პროცესებით, ცვლადადგილიან პროცედურებს პროგრამირების ენებში და სხვ. ისინი გვხდებიან ასევე გადაწერაში, ცოდნის წარმოდგენაში, პროგრამების ანალიზის და გარდაქმნის დროს. ამიტომ მათი ჩართვა შეზღუდვებიანი ლოგიკური პროგრამირების ჩარჩოში საინტერესო და სასარგებლო გაფართოებას მოგვცემს.
განაცხადში განხილული ენის კიდევ ერთი განსაკუთრებული მახასიათებელია ის, რომ ტერმებში დაიშვება განსაზღვრული და განუსაზღვრელი
აღწერის ოპერატორები რასელის იოტა და ბურბაკის ტაუ (რომელიც ჰილბერტის ეფსილონის სახელითაცაა ცნობილი).
ეკვაციონალური ატომი არის ტერმების ტოლობა. მიკუთვნების ატომი შემოფარგლავს მიმდევრობის და კონტექსტის ცვლადების შესაძლო მნიშვნელობების სიმრავლეს, შესაბამისად, მიმდევრობების რეგულარული ენით და კონტექსტების რეგულარული ენით. შეზღუდვები აიგება ეკვაციონალური და მიკუთვნების ატომებიდან უარყოფის, დიზიუნქციის და კონიუნქციის მეშვეობით.
შეზღუდვებში შემომავალი ის ტერმები, რომლებიც აღწერის ოპერატორებს შეიცავენ, რთულ შეზღუდვას კომპაქტურად ჩაწერენ და ხშირად საშუალებას იძლევიან ავერიდოთ უსარგებლო გამოყვანებს თუ გამოთვლებს.
ამგვარად განსაზღვრული შეზღუდვების ენა მოქნილი და გამომსახველობითია, მაგრამ მისი გამომსახველობითი ძალა უნდა შეიზღუდოს, რათა გამოთვლების ეფექტურად ჩატარების საშუალება გვქონდეს.
პროექტის ამოცანაა იპოვოს შეზღუდვების ისეთი სინტაქსური ფრაგმენტები, რომლებიც, ერთი მხრივ, საკმაოდ გამოსახველობითი არიან და, მეორე მხრივ, უშვებენ გადაწყვეტის და ამოხსნის ეფექტურ პროცედურებს. ამ ფრაგმენტებისთვის იგეგმება გადაწყვეტადობის და ამოხსნის ალგორითმების აგება, მათი თვისებების (გაჩერება, კორექტულობა, სისრულე) დამტკიცება და იმპლემენტაცია.
კვლევის მეორე მიმართულება ეხება პროგრამების კლაუზების და მიზნების ისეთი ფორმების მონახვას, რომლებიც გარანტიას იძლევიან, რომ გამოყვანის პროცესში მხოლოდ გადაწყვეტადი და სასრულად ამოხსნადი შეზღუდვები წარმოიშობა.
პროექტის მოსალოდნელ შედეგებს ორგვარი მნიშვნელობა ექნება. პირველი, ისინი გააფართოებენ შეზღუდვების ამოხსნების არსებულ
ფორმალიზმებს შეზღუდვების ახალი, ფართო კლასის შემოტანით და მისთვის გადაწყვეტის და ამოხსნის მეთოდების აგებით. მეორე, ისინი განავრცობენ შეზღუდვებიანი ლოგიკური პროგრამირების გამოყენების სფეროს იმ არეებზე, რომელთა მოდელირება ურანგო ტერმებით და მათი მიმდევრობებით აბსტრაგირებას მოითხოვს.