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