در منطق صوری ارضاپذیری هورن عبارت است از مسئلهٔ تعیین اینکه آیا مجموعهٔ مفروضی از عبارتهای هورن گزاره ای ارضا پذیر است یا نه. یک عبارت هورن عبارتی با حداکثر یک لفظ مثبت که سر عبارت نامیده می شود و هر تعدادی لفظهای منفی که بدنهٔ عبارت را تشکیل می دهد .یک فرمول هورن یک فرمول گزاره ایست که به وسیلهٔ پیوند دادن عبارت های هورن شکل یافته است.مسئلهٔ ارضاپذیری هورن در زمان چندجمله ای قابل حل است. یک الگور...