عبارت هورن

عبارت یا بند هورن (به انگلیسی: Horn clause) در منطق ریاضی و برنامه‌نویسی منطقی، یک فرمول منطقی دارای «فرم قاعده‌ای بخصوص» است، که این فرم بخصوص موجب ویژگی‌های مفیدی برای استفاده آن بندها در برنامه‌نویسی منطقی، مشخصات صوری، و نظریه مدل می‌شود. واژه «بند هورن» از اسم یک منطق‌دان به نام آلفرد هورن گرفته شده‌است، که اولین بار در سال ۱۹۵۱ به اهمیت این بندها اشاره کرد.

تعریف

یک بند هورن یک بند است (یک فصل از لیترال‌ها است) که حداکثر یک لیترال آن مثبت (یعنی غیرنقیض) است.

به صورت معکوس، یک فصل از لیترال‌ها که حداکثر یک لیترال منفی دارد یک «بند دوگان هورن» است.

یک بند معین (به انگلیسی: definite clause) یا بند هورن اکید یک بند هورن است که دقیقاً یک لیترال مثبت دارد، به بند معینی که هیچ لیترال منفی ندارد بند واحد (به انگلیسی: unit clause) می‌گویند، و به بند واحدی که متغیری ندارد واقعیت (به انگلیسی: fact) گفته می‌شود؛ و به بند هورنی که لیترال مثبت ندارد بند هدف (به انگلیسی: goal clause) گفته می‌شود (توجه کنید که بند خالی که شامل هیچ لیترالی نیست هم‌بند هدف است). این سه نوع بند هورن در مثال گزاره‌ای زیر نشان داده شده‌است:

	فرم فصلی	فرم پیامدی	خواندن بصری
بند معین Definite clause	¬p ∨ ¬q ∨ … ∨ ¬t ∨ u	u ← p ∧ q ∧ … ∧ t	assume that, if p and q and … and t all hold, then also u holds
واقعیت Fact	u	u	assume that u holds
بند هدف Goal clause	¬p ∨ ¬q ∨ … ∨ ¬t	false ← p ∧ q ∧ … ∧ t	show that p and q and … and t all hold

در حالت غیرگزاره‌ای، همه متغیرها در بند به صورت ضمنی سور عمومی دارند، که بازه آن سور، کل بند است؛ بنابراین، مثال:

¬ human(X) ∨ mortal(X)

به معنی

∀X(¬ human(X) ∨ mortal(X))

است که به صورت منطقی معادل است با:

∀X (human(X) → mortal(X))

اهمیت

بندهای هورن یک نقش اساسی در منطق سازندگی یا منطق محاسباتی دارند. این بندها در اثبات قضیه خودکار هم مهم اند زیرا در رزلوشن مرتبه اول از آن‌ها استفاده می‌شود، زیرا حل‌مسئله (ناشی از رزلوشن) دو بند هورن خودش یک بند هورن است، و حل‌مسئله یک بند هدف و یک بند معین، یک بند هدف است. این ویژگی‌های بندهای هورن، منجر به کارایی بالاتر در اثبات یک قضیه می‌شود (که به صورت نقیض یک بند هدف نمایش می‌یابد).

در زمینه پیچیدگی محاسباتی هم توجه زیادی به بندهای هورن گزاره‌ای شده‌است. مسئله یافتن انتساب مقدار درستی برای درست ساختن یک عطف از بندهای هورن گزاره‌ای، در واقع یک مسئله p-کامل است، که در زمان خطی قابل حل است، و گاهی HORNSAT نامیده می‌شود (اما مسئله صدق‌پذیری بولی بدون محدودیت یک مسئله NP-کامل است).

برنامه‌نویسی منطقی

بندهای هورن همچنین مبنای برنامه‌نویسی منطقی هستند، که در آن نوع برنامه‌نویسی نوشتن بندهای معین به صورت فرم پیامد منطقی یک موضوع معمول است:

(p ∧ q ∧ … ∧ t) → u

در واقع رزلوشن یک بند هدف با یک بند معین برای ایجاد یک بند هدف جدید مبنای قاعده استنتاج رزلوشن SLD است، که از آن برای پیاده‌سازی برنامه‌های منطقی در زبان برنامه‌نویسی پرولوگ استفاده می‌شود.

در برنامه‌نویسی منطقی یک بند معین به صورت یک «فرایند کاهش هدف» عمل می‌کند. برای مثال، بند هورن نوشته شده در بالا به صورت فرایند زیر عمل می‌کند:

to show u, show p and show q and … and show t.

اما برای تأکید بیشتر روی استفاده معکوس از بند، معمولاً در فرم معکوس نوشته می‌شود:

u ← (p ∧ q ∧ … ∧ t)

در زبان پرولوگ، عبارت بالا به این صورت نوشته می‌شود:

u :- p, q, ..., t.

در برنامه‌نویسی منطقی و دیتالاگ، محاسبه و ارزیابی پرسمان به وسیله نمایش نقیض مسئله‌ای که می‌خواهد حل شود، به صورت یک بند هدف انجام می‌شود. برای مثال، مسئله حل عطف سور وجودی برای لیترال‌های مثبت زیر:

∃X (p ∧ q ∧ … ∧ t)

توسط نقیض مسئله (انکار اینکه یک جواب برای آن وجود دارد) نمایش می‌یابد، و سپس آن را به صورت فرم معادل منطقی از یک بند هدف نمایش می‌دهند:

∀X (false ← p ∧ q ∧ … ∧ t)

که در پرولوگ به صورت زیر نوشته می‌شود:

:- p, q, ..., t.

حل مسئله تا زمان یافتن یک تناقض ادامه می‌یابد، که آن تناقض به صورت بند خالی (یا «false») نمایش می‌یابد. راه‌حل مسئله همان «جایگزینی ترم‌ها» برای متغیرهای موجود در بند هدف است، که این موضوع از «اثبات آن تناقض» قابل استخراج است. در این روش، بندهای هدف مشابه پرسمان‌های عطفی در پایگاه‌داده‌های رابطه‌ای هستند، و منطق بند هورن از نظر قدرت محاسباتی با ماشین تورینگ جهانی معادل است.

در واقع نمادگذاری پرولوگ ابهام دارد، و عبارت «بند هدف» گاهی به صورت مبهم استفاده می‌شود. متغیرهای موجود در بند هدف را هم به صورت سور عمومی و هم سور وجودی داده شده می‌توان خواند، و به دست آوردن «false» را می‌توان یا به صورت اشتقاق یک تناقض یا به صورت اشتقاق یک جواب موفق از مسئله‌ای که قصد حل آن را داریم، قابل تفسیر است.

آقای ون آمدن و کوالسکی (۱۹۷۶) ویژگی‌های نظری مدل را برای بندهای هورن در زمینه برنامه‌نویسی منطقی وارسی کردند، و نشان دادند که هر مجموعه از بندهای معین D یک مدل حداقلی یکتا M دارد. یک فرمول اتمی A فقط و فقط موقعی توسط D پیامد منطقی دارد که A در M درست باشد. این به معنی آن است که یک مسئله P که توسط عطف سور وجودی داده شده از لیترال‌های مثبت نمایش می‌یابد فقط و فقط وقتی توسط D پیامد منطقی دارد که P در M درست باشد. معناشناسی مدل حداقلی برای بندهای هورن مبنای معناشناسی مدل ثابت برای برنامه‌های منطقی است.

یادداشت

↑ Like in resolution theorem proving, intuitive meanings "show φ" and "assume ¬φ" are synonymous (indirect proof); they both correspond to the same formula, viz. ¬φ. This way, a mechanical proving tool needs to maintain only one set of formulas (assumptions), rather than two sets (assumptions and (sub)goals).
↑ Like in resolution theorem proving, intuitive meanings "show φ" and "assume ¬φ" are synonymous (indirect proof); they both correspond to the same formula, viz. ¬φ. This way, a mechanical proving tool needs to maintain only one set of formulas (assumptions), rather than two sets (assumptions and (sub)goals).

پانویس

↑ Horn, Alfred (1951). "On sentences which are true of direct unions of algebras". Journal of Symbolic Logic. 16 (1): 14–21. doi:10.2307/2268661. JSTOR 2268661.
↑ Makowsky (1987). "Why Horn Formulas Matter in Computer Science: Initial Structures and Generic Examples" (PDF). Journal of Computer and System Sciences. 34 (2–3): 266–292. doi:10.1016/0022-0000(87)90027-4.
↑ Buss, Samuel R. (1998). "An Introduction to Proof Theory". In Samuel R. Buss (ed.). Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics. Vol. 137. Elsevier B.V. pp. 1–78. doi:10.1016/S0049-237X(98)80016-5. ISBN 978-0-444-89840-1. ISSN 0049-237X.
↑ Lau & Ornaghi (2004). "Specifying Compositional Units for Correct Program Development in Computational Logic". Lecture Notes in Computer Science. 3049: 1–29. doi:10.1007/978-3-540-25951-0_1. ISBN 978-3-540-22152-4.
↑ Dowling, William F.; Gallier, Jean H. (1984). "Linear-time algorithms for testing the satisfiability of propositional Horn formulae". Journal of Logic Programming. 1 (3): 267–284. doi:10.1016/0743-1066(84)90014-1.
↑ van Emden, M. H.; Kowalski, R. A. (1976). "The semantics of predicate logic as a programming language" (PDF). Journal of the ACM. 23 (4): 733–742. CiteSeerX 10.1.1.64.9246. doi:10.1145/321978.321991.

منابع

مشارکت‌کنندگان ویکی‌پدیا. «Horn clause». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۲۱ مهٔ ۲۰۲۱.

[5] Like in resolution theorem proving, intuitive meanings "show φ" and "assume ¬φ" are synonymous (indirect proof); they both correspond to the same formula, viz. ¬φ. This way, a mechanical proving tool needs to maintain only one set of formulas (assumptions), rather than two sets (assumptions and (sub)goals).

[6] Like in resolution theorem proving, intuitive meanings "show φ" and "assume ¬φ" are synonymous (indirect proof); they both correspond to the same formula, viz. ¬φ. This way, a mechanical proving tool needs to maintain only one set of formulas (assumptions), rather than two sets (assumptions and (sub)goals).

[onsentences-1] Horn, Alfred (1951). "On sentences which are true of direct unions of algebras". Journal of Symbolic Logic. 16 (1): 14–21. doi:10.2307/2268661. JSTOR 2268661.

[makowsky-2] Makowsky (1987). "Why Horn Formulas Matter in Computer Science: Initial Structures and Generic Examples" (PDF). Journal of Computer and System Sciences. 34 (2–3): 266–292. doi:10.1016/0022-0000(87)90027-4.

[3] Buss, Samuel R. (1998). "An Introduction to Proof Theory". In Samuel R. Buss (ed.). Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics. Vol. 137. Elsevier B.V. pp. 1–78. doi:10.1016/S0049-237X(98)80016-5. ISBN 978-0-444-89840-1. ISSN 0049-237X.

[4] Lau & Ornaghi (2004). "Specifying Compositional Units for Correct Program Development in Computational Logic". Lecture Notes in Computer Science. 3049: 1–29. doi:10.1007/978-3-540-25951-0_1. ISBN 978-3-540-22152-4.

[dowling-7] Dowling, William F.; Gallier, Jean H. (1984). "Linear-time algorithms for testing the satisfiability of propositional Horn formulae". Journal of Logic Programming. 1 (3): 267–284. doi:10.1016/0743-1066(84)90014-1.

[emdenkowalski-8] van Emden, M. H.; Kowalski, R. A. (1976). "The semantics of predicate logic as a programming language" (PDF). Journal of the ACM. 23 (4): 733–742. CiteSeerX 10.1.1.64.9246. doi:10.1145/321978.321991.