In the early 11th century Ibn Sīnā was teaching his students a recursive algorithm for finding completions of incomplete proofs. In section 9.6 of Qiyās (from his Šifā') he gives the algorithm in enough detail to allow translation into an abstract state machine [2], and he promises a fuller account in his 'Appendices' (now lost if they were ever written). At one point the algorithm relies on an oracle for surveying existing knowledge, where similar modern algorithms normally backtrack through a list of axioms given in advance [1]. The algorithm might be the world's first significant non-numerical algorithm. Ibn Sīnā shows no awareness of any connection to numerical algorithms known in his time, and (unlike Al-Khwārizmī in the 9th century [3]) he makes no attempt to verify the correctness of the algorithm. [1] Egon Börger and Dean Rosenzweig, 'A mathematical definition of full Prolog', Science of Computer Programming 24 (1995) 249-286. [2] Wilfrid Hodges, 'Ibn Sīnā on analysis: 1. Proof search', in Fields of logic and computation: Essays dedicated to Yuri Gurevich on the occasion of his 70th birthday, ed. Andreas Blass, Nachum Dershowitz and Wolfgang Reisig, Springer Lecture Notes in Computer Science 6300, Berlin 2010, pp. 354-404. [3] Roshdi Rashed, Al-Khwārizmī, Le commencement de l'algèbre, Blanchard, Paris 2007.