ريتشارد والدينجر

تعاون والدينجر مع كورديل غرين ، وروبرت ييتس، وجيف روليفسون، ويان ديركسن في تطوير QA4 ، وهي لغة ذكاء اصطناعي شبيهة بلغة PLANNER ، مُصممة للتخطيط التلقائي وإثبات النظريات. ^{[ 5 ]} قدمت QA4 مفهوم السياق، بالإضافة إلى مفهوم التوحيد الترابطي-التبديلي، مما جعل بديهيات التجميع والتبديل للمؤثرات غير ضرورية، بل وغير قابلة للتعبير. طبقوا هذه اللغة على تخطيط روبوت SRI، المسمى Shakey . استخدم والدينجر، بالتعاون مع بيرني إلسباس وكارل ليفيت، لغة QA4 للتحقق من البرامج (إثبات أن البرنامج يؤدي وظيفته كما هو مُفترض)، وحصل على عمليات تحقق تلقائية لخوارزمية التوحيد وبرنامج FIND الخاص بهوار .

بينما تناولت أطروحة والدينجر توليف البرامج التطبيقية، التي تُنتج مخرجات دون آثار جانبية، انتقل والدينجر بعد ذلك إلى توليف البرامج الإجرائية، التي تجمع بين الأمرين. ^{[ 6 ]} ولمعالجة مشكلة تحقيق أهداف متضاربة في آنٍ واحد، قدّم مفهوم انحدار الأهداف، المُستمد من أعمال سابقة في التحقق من البرامج قام بها كلٌ من فلويد ، وكينغ، وهوار ، وديجكسترا . ولأن البرامج الإجرائية تُشابه الخطط، فقد كان هذا النهج قابلاً للتطبيق أيضاً على مسائل التخطيط الكلاسيكية في الذكاء الاصطناعي.

بالتعاون مع زوهار مانا من جامعة ستانفورد ، طوّر والدينجر طريقة الاستدلال غير الشرطي، وهي شكل من أشكال الاستدلال لا يتطلب ترجمة الجمل المنطقية إلى صيغة شرطية مقيدة. لم تكن الترجمة مكلفة فحسب، بل كانت تُعقّد أحيانًا برهان النظرية الناتجة بشكل كبير؛ وقد تم تجاوز هذه المشاكل بالقاعدة الجديدة. طبّقا القاعدة على الورق لإنتاج توليفة مفصلة لخوارزمية التوحيد. وفي ورقة بحثية منفصلة، ​​قاما بتوليف خوارزمية جديدة للجذر التربيعي؛ ووجدا أن مفهوم البحث الثنائي يظهر تلقائيًا من خلال تطبيق واحد لقاعدة الاستدلال على تحديد الجذر التربيعي. ^{[ 7 ] [ 8 ]}

تم دمج بعض أفكار مانا ووالدينجر حول إثبات النظريات في تصميم برنامج إثبات النظريات SNARK الذي ابتكره مارك ستيكل . استخدم باحثون من وكالة ناسا ، بقيادة مايك لوري، برنامج SNARK في تطوير بيئة البرمجيات Amphion، التي استُخدمت بدورها لإنشاء برامج لتحليل بيانات مهمات ناسا لصالح علماء الفلك الكوكبي. كما استُخدمت برمجيات أُنشئت تلقائيًا بواسطة Amphion لتخطيط التصوير الفوتوغرافي لمهمة كاسيني-هويجنز التابعة لناسا؛ ولعل هذا هو التطبيق العملي الأبرز حتى الآن للبرمجيات التي تُنشأ تلقائيًا باستخدام الأساليب الاستنتاجية.

أدمج معهد كيستريل نظام SNARK في بيئة تطوير البرمجيات Specware، التي استخدمها والدينجر للتحقق من صحة البديهيات من الدرجة الأولى للغة DAML ، وهي لغة ترميز وكلاء DARPA ، ولغة OWL التي تلتها . كشف نظام SNARK عن تناقضات ليس فقط في بديهيات DAML، بل أيضًا في بديهيات لغة KIF الأساسية ، التي استندت إليها بديهيات DAML. وقد عمل والدينجر مؤخرًا على تطبيق الأساليب الاستنتاجية للإجابة عن أسئلة في الجغرافيا وعلم الأحياء وتحليل المعلومات الاستخباراتية. وبالتعاون مع معهد كيستريل، يستخدم نظام SNARK للتحقق من صحة بروتوكولات الأمان.