1956, RAND Corporation: תוכנית שהוכיחה משפטים לוגיים
אלן ניואל, הרברט סיימון וקליף שו החלו לפתח את התיאורטיקן הלוגי כבר ב-1955, עוד לפני שהמונח "בינה מלאכותית" נטבע כלל, ועבדו עליו ב-RAND Corporation שבסנטה-מוניקה, קליפורניה. ניואל גייס את שו, מתמטיקאי ומתכנת ב-RAND, כדי לממש בפועל את רעיונו של סיימון: תוכנית-מחשב שתדמה תהליך-חשיבה אנושי — לא רק תחשב, אלא תוכיח משפטים לוגיים כמו מתמטיקאי בשר-ודם. שו כתב את התוכנית בשפת IPL (Information Processing Language) שהומצאה במיוחד עבור המשימה הזו. בינואר 1956 סיפר סיימון לכיתת-תלמידים-לתואר-שני: "מעל חג-המולד, אל ניואל ואני המצאנו מכונה חושבת" — הצהרה נועזת עוד לפני שהתוכנית אף הושלמה במלואה.
38 מתוך 52: מה בדיוק היא הוכיחה
התוכנית הושלמה ב-1956, ובמשימתה המרכזית — הוכחת משפטים מתוך הפרק השני של Principia Mathematica, יצירת-המופת המתמטית של וייטהד וראסל — היא הוכיחה 38 מתוך 52 המשפטים הראשונים. במשפט 2.85 היא אף עשתה יותר מכך: מצאה הוכחה קצרה ואלגנטית יותר מזו שוייטהד וראסל עצמם ניסחו ביד. סיימון הראה את ההוכחה החדשה לראסל עצמו, שלפי התיעוד "הגיב בהתלהבות". ניואל וסיימון ניסו לפרסם את ההוכחה החדשה בכתב-העת Journal of Symbolic Logic, אך זו נדחתה — בנימוק שהוכחה חדשה למשפט אלמנטרי אינה נחשבת-דיה, מבלי שהעורכים שמו-לב שאחד ה"מוכיחים" היה בעצם תוכנית-מחשב.
חיפוש היוריסטי ו-IPL: החידוש הטכני
החידוש הטכני המרכזי היה חיפוש היוריסטי: במקום לבדוק כל שביל אפשרי בעץ-ההוכחות העצום, התוכנית השתמשה בכללי-אצבע שקיצצו את מרחב-החיפוש לגודל בר-ניהול. כדי לממש זאת כתב שו את שפת ה-IPL — שפת-תכנות המבוססת על עיבוד-רשימות סמלי, אותו רעיון-יסוד שעליו נשען מאוחר יותר גם ה-Lisp של ג'ון מקארתי, שפה שנותרה מרכזית במחקר-AI עשרות שנים.
דארטמות', קיץ 1956: קבלת-פנים פושרת
בקיץ 1956 הציגו ניואל וסיימון את התיאורטיקן הלוגי בוועידת דארטמות', האירוע שבו נטבע המונח "בינה מלאכותית". להפתעתם, ההצגה זכתה לקבלת-פנים פושרת יחסית — לפי ההיסטוריונית פמלה מקורדוק, "העדות היא שאיש מלבד ניואל וסיימון עצמם לא חש בחשיבות ארוכת-הטווח של מה שהם עשו" באותו רגע.
המורשת: מ"התיאורטיקן הלוגי" ועד תוכנות-ההוכחה של היום
התיאורטיקן הלוגי מוגדר בעקביות כ"תוכנית-הבינה-המלאכותית הראשונה בהיסטוריה" — התוכנית הראשונה שנבנתה במכוון לבצע הסקה אוטומטית. היא מתוארת גם כהופעת-הבכורה של תיאוריה חדשה על התודעה — מודל-עיבוד-המידע; ההיסטוריונית פמלה מקורדוק כתבה שהתפיסה הזו תהפוך למרכזית בעבודתם המאוחרת של ניואל וסיימון, ולדעתם מרכזית להבנת התודעה במאה ה-20 כשם שעקרון הברירה הטבעית היה להבנת הביולוגיה במאה ה-19. קוד-המקור המקורי נחשב אבוד במשך עשורים, עד שדוח-RAND המקורי מ-1956, P-868, שכותרתו המלאה "The Logic Theory Machine: A Complex Information Processing System", אותר ופורסם מחדש ב-2017 בידי פרויקט Theorem Prover Museum. ניואל וסיימון המשיכו את שיתוף-הפעולה שלהם לתוכניות-המשך משפיעות נוספות — בהן General Problem Solver ומאוחר יותר Soar — שהניחו יחד יסוד לפסיכולוגיה הקוגניטיבית המודרנית.