عبارت هورن: تفاوت میان نسخه‌ها
بدون خلاصۀ ویرایش برچسب‌ها: افزودن پیوند بیرونی به جای ویکی‌پیوند ویرایشگر دیداری |
بدون خلاصۀ ویرایش |
||
| خط ۱: | خط ۱: | ||
'''عبارت''' یا '''بند هورن''' {{به انگلیسی|Horn clause}} در [[منطق ریاضی]] و [[برنامه‌نویسی منطقی]]، یک فرمول منطقی از فرم قاعده‌ای بخصوص است، که این فرم به آن بندها ویژگی‌های مفیدی برای استفاده در برنامه‌نویسی منطقی، مشخصات |
'''عبارت''' یا '''بند هورن''' {{به انگلیسی|Horn clause}} در [[منطق ریاضی]] و [[برنامه‌نویسی منطقی]]، یک فرمول منطقی از فرم قاعده‌ای بخصوص است، که این فرم به آن بندها ویژگی‌های مفیدی برای استفاده در برنامه‌نویسی منطقی، [[:en:Formal_specification|مشخصات صوری]]، و [[نظریه مدل]] می‌دهد. واژه «بند هورن» از اسم منطق‌دانی به نام [[:en:Alfred_Horn|آلفرد هورن]] گرفته شده است، که اولین بار در سال 1951 به اهمیت این عبارات اشاره کرد.<ref name="onsentences">{{cite journal|last=Horn|first=Alfred|author-link=Alfred Horn|year=1951|title=On sentences which are true of direct unions of algebras|journal=[[Journal of Symbolic Logic]]|volume=16|pages=14–21|doi=10.2307/2268661|jstor=2268661|number=1}}</ref> |
||
== تعریف == |
== تعریف == |
||
یک بند هورن یک بند است (یک فصل از لیترال‌ها است) که حداکثر یک لیترال آن مثبت (یعنی |
یک بند هورن یک [[بند (منطق)|بند]] است (یک [[فصل منطقی|فصل]] از [[لیترال (منطق ریاضی)|لیترال‌ها]] است) که حداکثر یک لیترال آن مثبت (یعنی [[نقیض|غیرنقیض]]) است. |
||
به صورت معکوس، یک فصل از لیترال ها که حداکثر یک لیترال منفی دارد یک بند دوگان هورن است. |
به صورت معکوس، یک فصل از لیترال ها که حداکثر یک لیترال منفی دارد یک بند دوگان هورن است. |
||
یک '''بند معین''' {{به انگلیسی|definite clause}} یا '''بند هورن اکید''' یک بند هورن است که دقیقا یک لیترال مثبت دارد، به بند معینی که هیچ لیترال منفی ندارد '''بند واحد''' {{به انگلیسی|unit clause}} می گویند، و به بند واحدی که متغیری ندارد '''واقعیت''' {{به انگلیسی|fact}} گفته می شود؛ و به بند هورنی که لیترال مثبت ندارد '''بند هدف''' {{به انگلیسی|goal clause}} گفته می شود (توجه کنید که بند خالی که شامل هیچ لیترالی نیست هم بند هدف است). این سه نوع بند هورن در مثال گزاره‌ای زیر نشان داده شده است: |
یک '''بند معین''' {{به انگلیسی|definite clause}} یا '''بند هورن اکید''' یک بند هورن است که دقیقا یک لیترال مثبت دارد،<ref name="makowsky">{{cite journal|last1=Makowsky|year=1987|title=Why Horn Formulas Matter in Computer Science: Initial Structures and Generic Examples|url=https://core.ac.uk/download/pdf/82190596.pdf|journal=Journal of Computer and System Sciences|volume=34|issue=2–3|pages=266–292|doi=10.1016/0022-0000(87)90027-4}}</ref> به بند معینی که هیچ لیترال منفی ندارد '''بند واحد''' {{به انگلیسی|unit clause}} می گویند،<ref>{{cite book|isbn=978-0-444-89840-1|issn=0049-237X|editor=Samuel R. Buss|title=Handbook of Proof Theory|publisher=Elsevier B.V|series=Studies in Logic and the Foundations of Mathematics|volume=137|year=1998|last1=Buss|first1=Samuel R.|contribution=An Introduction to Proof Theory|pages=1–78|contribution-url=http://www.sciencedirect.com/science/article/pii/S0049237X98800165|doi=10.1016/S0049-237X(98)80016-5}}</ref> و به بند واحدی که متغیری ندارد '''واقعیت''' {{به انگلیسی|fact}} گفته می شود؛<ref>{{cite journal|last1=Lau & Ornaghi|year=2004|title=Specifying Compositional Units for Correct Program Development in Computational Logic.|journal=Lecture Notes in Computer Science|volume=3049|pages=1–29|doi=10.1007/978-3-540-25951-0_1|isbn=978-3-540-22152-4}}</ref> و به بند هورنی که لیترال مثبت ندارد '''بند هدف''' {{به انگلیسی|goal clause}} گفته می شود (توجه کنید که بند خالی که شامل هیچ لیترالی نیست هم بند هدف است). این سه نوع بند هورن در مثال [[:en:Propositional_formula|گزاره‌ای]] زیر نشان داده شده است: |
||
{|class="wikitable" |
{|class="wikitable" |
||
|- |
|- |
||
! |
! |
||
!فرم فصلی |
|||
!Disjunction form |
|||
!فرم پیامدی |
|||
![[Material conditional|Implication]] form |
|||
!خواندن بصری |
|||
!Read intuitively as |
|||
|- align="center" |
|- align="center" |
||
!بند معین |
|||
Definite clause |
|||
|¬''p'' ∨ ¬''q'' ∨ ... ∨ ¬''t'' ∨ ''u'' |
|¬''p'' ∨ ¬''q'' ∨ ... ∨ ¬''t'' ∨ ''u'' |
||
|| ''u'' ← ''p'' ∧ ''q'' ∧ ... ∧ ''t'' |
|| ''u'' ← ''p'' ∧ ''q'' ∧ ... ∧ ''t'' |
||
|| assume that,<BR>if ''p'' and ''q'' and ... and ''t'' all hold, then also ''u'' holds |
|| assume that,<BR>if ''p'' and ''q'' and ... and ''t'' all hold, then also ''u'' holds |
||
|-align="center" |
|-align="center" |
||
!واقعیت |
|||
!Fact |
|||
Fact |
|||
|''u'' |
|''u'' |
||
||''u'' |
||''u'' |
||
||assume that<BR>''u'' holds |
||assume that<BR>''u'' holds |
||
|-align="center" |
|-align="center" |
||
!بند هدف |
|||
Goal clause |
|||
| ¬''p'' ∨ ¬''q'' ∨ ... ∨ ¬''t'' |
| ¬''p'' ∨ ¬''q'' ∨ ... ∨ ¬''t'' |
||
|| ''false'' ← ''p'' ∧ ''q'' ∧ ... ∧ ''t'' |
|| ''false'' ← ''p'' ∧ ''q'' ∧ ... ∧ ''t'' |
||
|| show that<BR>''p'' and ''q'' and ... and ''t'' all hold <ref group=note>Like in [[Resolution_(logic)#A_resolution_technique|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).</ref> |
|| show that<BR>''p'' and ''q'' and ... and ''t'' all hold <ref group=note>Like in [[Resolution_(logic)#A_resolution_technique|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).</ref> |
||
|} |
|} |
||
در حالت |
در حالت [[منطق مرتبه اول|غیرگزاره‌ای]]، همه متغیرها<ref group="note">Like in [[Resolution_(logic)#A_resolution_technique|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).</ref> در بند به صورت ضمنی [[سور عمومی]] دارند، که بازه آن سور، کل بند است. بنابراین، برای مثال: |
||
:¬ ''human''(''X'') ∨ ''mortal''(''X'') |
:¬ ''human''(''X'') ∨ ''mortal''(''X'') |
||
نسخهٔ ۲۱ مهٔ ۲۰۲۱، ساعت ۱۳:۵۶
عبارت یا بند هورن (به انگلیسی: Horn clause) در منطق ریاضی و برنامه‌نویسی منطقی، یک فرمول منطقی از فرم قاعده‌ای بخصوص است، که این فرم به آن بندها ویژگی‌های مفیدی برای استفاده در برنامه‌نویسی منطقی، مشخصات صوری، و نظریه مدل می‌دهد. واژه «بند هورن» از اسم منطق‌دانی به نام آلفرد هورن گرفته شده است، که اولین بار در سال 1951 به اهمیت این عبارات اشاره کرد.[۱]
تعریف
یک بند هورن یک بند است (یک فصل از لیترال‌ها است) که حداکثر یک لیترال آن مثبت (یعنی غیرنقیض) است.
به صورت معکوس، یک فصل از لیترال ها که حداکثر یک لیترال منفی دارد یک بند دوگان هورن است.
یک بند معین (به انگلیسی: 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 [note ۱] |
در حالت غیرگزاره‌ای، همه متغیرها[note ۲] در بند به صورت ضمنی سور عمومی دارند، که بازه آن سور، کل بند است. بنابراین، برای مثال:
- ¬ 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» را می توان یا به صورت اشتقاق یک تناقض یا به صورت اشتقاق یک جواب موفق از مسئله‌ای که قصد حل آن را داریم، قابل تفسیر است.
ون امدن و کوالسکی (1976) ویژگی‌های نظری مدل را برای بندهای هورن در زمینه برنامه‌نویسی منطقی وارسی کردند، و نشان دادند که هر مجموعه از بندهای معین 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.
- ↑ 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». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۲۱ مهٔ ۲۰۲۱.