بند هورن

في المنطق الرياضي والبرمجة المنطقية ، تُعرف عبارة هورن بأنها صيغة منطقية ذات شكل يشبه القاعدة، مما يمنحها خصائص مفيدة للاستخدام في البرمجة المنطقية، والمواصفات الرسمية ، والجبر الشامل ، ونظرية النماذج . سُميت عبارات هورن نسبةً إلى عالم المنطق ألفريد هورن ، الذي أشار لأول مرة إلى أهميتها في عام 1951. ^{[ 1 ]}

جملة هورن هي جملة انفصالية ( فصل بين حرفين ) تحتوي على حرف واحد إيجابي على الأكثر، أي غير منفي .

وعلى العكس من ذلك، فإن الفصل بين المتغيرات الحرفية مع متغير حرفي واحد منفي على الأكثر يسمى جملة هورن المزدوجة .

^{[ 2 ]} جملة هورن التي تحتوي على متغير إيجابي واحد فقط هي جملة محددة أو جملة هورن صارمة ؛ ^{[ 3 ]} الجملة المحددة التي لا تحتوي على متغيرات سلبية هي جملة وحدة ؛ [4] جملة الوحدة التي لا تحتوي على متغيرات هي حقيقة ؛ ^{[ 5 ]} جملة هورن التي لا تحتوي على متغير إيجابي هي جملة هدف . الجملة الفارغة، التي لا تحتوي على أي متغيرات (وهي مكافئة لـ "خطأ" )، هي جملة هدف. يوضح المثال التالي هذه الأنواع الثلاثة من جمل هورن :

تُحدد جميع المتغيرات في الجملة ضمنيًا بشكل شامل ، بحيث يكون نطاقها هو الجملة بأكملها. على سبيل المثال:

يرمز إلى:

وهو ما يعادل منطقياً ما يلي:

تُعتبر عبارات هورن أيضًا أساسًا للبرمجة المنطقية ، حيث يشيع كتابة العبارات المحددة في شكل استلزام :

في الواقع، إن حل عبارة الهدف مع عبارة محددة لإنتاج عبارة هدف جديدة هو أساس قاعدة الاستدلال لحل SLD ، المستخدمة في تنفيذ لغة البرمجة المنطقية Prolog .

في البرمجة المنطقية، تعمل العبارة المحددة كإجراء لاختزال الهدف. على سبيل المثال، تعمل عبارة هورن المكتوبة أعلاه كإجراء:

وللتأكيد على هذا الاستخدام العكسي للعبارة، غالباً ما تُكتب بالشكل العكسي:

في لغة برولوج، يُكتب هذا على النحو التالي:

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

في البرمجة المنطقية، عبارة الهدف، التي لها الشكل المنطقي

يمثل هذا نفيًا لمشكلةٍ ما. أما المشكلة نفسها فهي عبارة عن اقتران كمي وجودي لقيم موجبة:

لا تحتوي صيغة لغة برولوج على محددات كمية صريحة، وتُكتب بالشكل التالي:

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

هذه الصيغة غامضة، إذ يمكن قراءتها إما كبيان للمشكلة أو كبيان لنفيها. ومع ذلك، كلا القراءتين صحيحتان. في كلتا الحالتين، يُختزل حل المشكلة إلى استنتاج العبارة الفارغة. في صيغة برولوج، يُكافئ هذا استنتاج:

:- حقيقي .

إذا فُسِّرَتْ عبارة الهدف الرئيسية على أنها نفي للمشكلة، فإن العبارة الفارغة تُمثِّل خطأً، وبرهان العبارة الفارغة يُفنِّد نفي المشكلة. أما إذا فُسِّرَتْ عبارة الهدف الرئيسية على أنها المشكلة نفسها، فإن العبارة الفارغة تُمثِّل صوابًا ، وبرهان العبارة الفارغة يُثبت أن للمشكلة حلًا.

يتمثل حل المشكلة في استبدال المصطلحات بالمتغيرات X في عبارة الهدف الرئيسية، والتي يمكن استخلاصها من برهان الاستدلال. عند استخدامها بهذه الطريقة، تُشبه عبارات الهدف الاستعلامات الاقترانية في قواعد البيانات العلائقية ، وتُعادل منطق عبارة هورن في القدرة الحسابية آلة تورينج العالمية .

درس فان إمدن وكوالسكي (1976) خصائص نظرية النماذج لعبارات هورن في سياق البرمجة المنطقية، موضحين أن لكل مجموعة من العبارات المحددة D نموذجًا أدنى فريدًا M. وتُستنتج الصيغة الذرية A منطقيًا من D إذا وفقط إذا كانت A صحيحة في M. ويترتب على ذلك أن المسألة P المُمثلة باقتران وجودي كمي من المتغيرات الموجبة تُستنتج منطقيًا من D إذا وفقط إذا كانت P صحيحة في M. وتُعد دلالات النموذج الأدنى لعبارات هورن أساسًا لدلالات النموذج المستقر للبرامج المنطقية. ^{[ 9 ]}

• بنود هورن المقيدة
• حساب القضايا

• بوريس، ستانلي؛ سانكابانافار، إتش بي، محرران. (1981). دورة في الجبر الشامل . سبرينغر-فيرلاغ. ISBN 0-387-90578-2.
• بوس، صموئيل ر. (1998). "مقدمة في نظرية البرهان" . في: صموئيل ر. بوس (محرر). دليل نظرية البرهان . دراسات في المنطق وأسس الرياضيات. المجلد  137. دار النشر إلسيفير، الصفحات 1-78. doi : 10.1016 / S0049-237X(98)80016-5 . ISBN  978-0-444-89840-1ISSN 0049-237X​​ 
• تشانغ، تشين تشونغ ؛ كيسلر، هـ. جيروم (1990) [1973]. نظرية النماذج . دراسات في المنطق وأسس الرياضيات (  الطبعة الثالثة). إلسيفير. ISBN 978-0-444-88054-3.
• داولينج، ويليام ف.؛ جالييه، جان هـ. (1984). "خوارزميات خطية لاختبار قابلية إرضاء صيغ هورن الافتراضية" . مجلة برمجة المنطق . 1 (3): 267-284 . doi : 10.1016/0743-1066(84)90014-1 .
• فان إمدن، إم إتش ؛ كوالسكي، آر إيه (1976). "دلالات منطق المسند كلغة برمجة" (ملف PDF) . مجلة ACM . 23 (4): 733-742 . CiteSeerX 10.1.1.64.9246 . doi : 10.1145/321978.321991 . S2CID 11048276 .  
• هورن، ألفريد (1951). " حول الجمل الصحيحة في الاتحادات المباشرة للجبر". مجلة المنطق الرمزي . 16 (1): 14-21 . doi : 10.2307/2268661 . JSTOR 2268661. S2CID 42534337 .  
• لاو، كونغ كيو؛ أورناغي، ماريو (2004). "تحديد الوحدات التركيبية لتطوير البرامج بشكل صحيح في المنطق الحسابي". تطوير البرامج في المنطق الحسابي . سلسلة محاضرات في علوم الحاسوب. المجلد  3049. الصفحات 1-29 . doi : 10.1007/978-3-540-25951-0_1 . ISBN  978-3-540-22152-4.
• ماكوفسكي، جيه إيه (1987). "لماذا تُعدّ صيغ هورن مهمة في علوم الحاسوب: البنى الأولية والأمثلة العامة" (ملف PDF) . مجلة علوم الحاسوب والأنظمة . 34 ( 2-3 ): 266-292 . doi : 10.1016/0022-0000(87)90027-4 .