SNARK (teorema prover) - SNARK (theorem prover)

SNARK, (SRI ning yangi avtomatlashtirilgan mulohaza to'plami), a teorema prover ko'p navli uchun birinchi darajali mantiq ilovalar uchun mo'ljallangan sun'iy intellekt va dasturiy ta'minot, da ishlab chiqilgan Xalqaro SRI.

SNARKning asosiy xulosa chiqarish mexanizmlari qaror va paramodulyatsiya; Bundan tashqari, u ma'lum bir domenlar uchun ixtisoslashgan qarorlar protseduralarini taklif qiladi, masalan, Allenning vaqt oralig'i mantig'ini cheklovchi hal qiluvchi. Boshqa ko'plab teoremalardan farqli o'laroq, to'liq avtomatlashtirilgan (interaktiv bo'lmagan). SNARK qidiruv xatti-harakatlarini sozlash va shu bilan uning ishlashini muayyan dasturlarga moslashtirish uchun ko'plab strategik boshqaruvlarni taklif etadi. Bu, shuningdek, ko'p maqsadli mantiq va maxsus maqsadlar uchun mulohaza yuritish protseduralarini umumiy maqsadga muvofiq xulosalar bilan birlashtirish uchun qulayliklardan foydalanish bilan birga, uni katta da'volar uchun asos bo'lib xizmat qiladi.

SNARK-da mantiqiy komponent sifatida ishlatiladi NASA Aqlli tizimlar loyihasi. Bu yozilgan Umumiy Lisp va ostida mavjud Mozilla jamoat litsenziyasi.

Shuningdek qarang

Adabiyotlar

  • M. Stikel, R. Valdinger, M. Lowry, T. Pressburger va I. Underwood. "Subroutine kutubxonalaridan astronomik dasturlarning deduktiv tarkibi". Avtomatlashtirilgan chegirmalar bo'yicha o'n ikkinchi xalqaro konferentsiya materiallari (CADE-12), Nensi, Frantsiya, 1994 yil iyun, 341–355 betlar.
  • Richard Valdinger, Martin Reddi va Jennifer Dungan. "Bir nechta ma'lumot manbalarining deduktiv tarkibi. "2002 yil may oyida NASA SISM Intelligent System Project (Intelligent System Project) tadqiqot ma'lumotlarini tushunishga oid intellektual ma'lumotlarning rivojlanishi to'g'risida hisobot.
  • R, Valdinger, D. E. Appelt, J. Fray, D. J. Isroil, P. Jarvis, D. Martin, S. Rixeman, M. E. Stikel, M. Tayson, J. Xobbs va J. L. Dungan. "Bir nechta manbalardan deduktiv savolga javob berish. "ichida Savollarga javob berishning yangi yo'nalishlari, AAAI, 2004.
  • R. Valdinger, P. Jarvis va J. Dungan. "Bir nechta ma'lumot manbalarini xoreografiya qilish uchun chegirmadan foydalanish". Yilda Qidirish va olish uchun semantik veb-texnologiyalar, Sanibel oroli, Florida, 2003 yil oktyabr.

Tashqi havolalar