≡
فهرست:
نگارش(نحو) صورت و الگوریتم آن در منطق درآمدی یه منطق

نگارش (نحو) صورت و الگوریتم آن در منطق

منطق و فرامنطق

درآمد به منطق

روند ۶. نگارش(نحو) صورت و الگوریتم آن در منطق

۱- سرآغاز

۹- فرمول اتمی

۲- معرفی واژگان ابتدایی LP

۱۰- معرفی "≡"

۳- نگارش صورت

۱۱- شمارایی مجموعه فرمول‌ها

۴- روند نگارش صورت

۱۲- تصمیم پذیری فرمول خوش-ساخت در منطق گزاره‌ها

۵- تعریف بازگشتی صورت

۱۳- الگوریتمِ تصمیم پذیری فرمول

۶- مثال: نگارش لفظ

۱۴-  درخت پیکربندی فرمول

۷- فرمول‌ در منطق

۱۵- مثال برای درخت پیکربندی

۸- فرمول شماتیک

۱۶- شناسایی درخت فراکافت

■ سرآغاز

یادآوری : یک زبان صوری مجموعه‌ای از‌ واژگان ابتدایی همراه با فهرست محدود از قواعد، موسوم به قواعد ساخت است؛ به قسمی که به‌موجب این قواعد یک و فقط یک زیرمجموعه‌ ناتهی و سره از عبارت‌های زبان — موسوم به فرمول‌های خوش-ساخت — ساخته و متمایز گردد.

 هدف این یادداشت نگاه نزدیک به روند ساختن یک زبان صوری و نیز نشان دادن تصمیم پذیری و خوانش یکتای آن است. به‌عبارت‌دیگر، ارائه الگوریتمی که بتواند برای هر عبارت دلخواه زبان به پرسش "آیا این عبارت یک عبارت خوش- ساخت در آن زبان است یا نه؟" به‌طور صحیح پاسخ آری یا نه دهد. بنابراین، موردتوجه این یادداشت صرفاً نگارش صورت (لفظ) در زبان صوری است. [برای تعریف دقیق "رشته‌"، "زبان" و "عبارت" اینجا را ببینید.]

☚ مجموعه قواعد ساخت یک زبان صوری را نیز قواعد نگارش صورت (یا نحو زبان صوری) می‌نامند.

در بند بعد، یک زبان صوری را، که از این پس به آن LP می‌گوییم، خواهیم ساخت.

■ معرفی واژگان ابتدایی LP

واژگان ابتدایی LP سه مجموعه دوبه‌دو از هم جدا به‌قرار زیر است:

۱-

اتم‌ها: به هر یک از عناصر مجموعه

{p, q, r, s , t, }

یک اتم LP (یا فقط اتم) می‌گوییم. گرچه در اینجا فقط هفت اتم معرفی شده است ولی در صورت لزوم می‌توان با کاربرد اندیس، مانند

{p۱, p۲, . . ., pn}

به هر تعداد دلخواه از آن‌ها معرفی کرد. به‌طورکلی مجموعه اتم‌ها نامتناهی فرض می‌شود. گرچه شمارایی مجموعه اتم‌ها ضروری نیست ولی آن ‌را شمارا فرض می‌کنیم. بنابراین می‌توان مجموعه اتم‌ها را

{p۱, p۲, . . ., pn, . . .}

نیز در نظر گرفت.

۲- رابط‌ها: {~, ∧, ∨, ⊃}؛  [بجای نماد "•" نماد "∧" را برای رابط عطف بکار برده‌ایم.]
۳- نمادهای ویژه به قرار {) ,(} به‌عنوان ابزار وابسته زبانی برای پرهیز از چند خوانشی.

اجتماع سه مجموعه بالا، به شمول ثابت‌های ثابت‌های منطقی، را ΣLp نامیده و به رشته‌های‌ متناهی ΣLp عبارت‌های‌ زبان LP می‌گوییم. بنابراین،

p)r∧p و p∧q و نیز p

هر سه عبارت‌های LP هستند.

☚می‌توان هر نماد را با قرار دادن آن داخل دو گیومه نام‌گذاری کرد؛ مثل "~" (یا «~») و مانند آن.
☚در کتاب «{»، «}»، «[»، و «]» به‌عنوان نشانه‌های ویژه معرفی‌شده‌اند ولی همان‌طور که دیده می‌شود در LP وجود ندارند.
☚در کتاب رابط "≡" به‌عنوان یک واژه ابتدایی معرفی شده که در LP وجود ندارد. همان‌طور که خواهیم دید در LP رابط "≡" را به‌عنوان یک واژه تعریف‌شده به کارخواهیم برد.
 
ثابت منطقی: به هر یک از دو نماد "⏉"، "⏊" یک ثابت منطقی می‌گوییم و آن‌ها به واژگان ابتدایی می‌افزاییم و به ترتیب آن‌ها را «درستی» و «نادرستی» می‌خوانیم. در این قسمت این دونماد مورد توجه ما نیستند.

■ نگارش صورت

همان‌طور که در بالا آمد، مراد از نگارش صورت (تألیف لفظ) وضع قواعدی است تا به‌موجب آن‌ها یک و فقط یک زیرمجموعه‌ ناتهی و سره از عبارت‌های LP، که ازاین‌پس آن را ƒLp می‌نامیم، متمایز گردد.

■ روند نگارش صورت

قواعد عضویت در ƒLp و به‌عبارت‌دیگر، تعریف ƒLp را به روش موسوم به تعریف بازگشتی بیان می‌کنیم.  این روش فراوان در  ریاضیات، منطق و دانش کامپیوتر بکار بسته می‌شود. ویژگیِ این‌گونه تعریف، که به آن تعریف سازنده هم می‌گویند، پیدایش مصداق‌های معرَف (تعریف‌شده) در روند تعریف است.

هر تعریف بازگشتی در سه‌گام انجام می‌شود. بنابراین ƒLp را در سه گام به شرحی که خواهد آمد تعریف می‌کنیم. ولی، قبل از آن نیاز به گفتن یک نکته است و آن اینکه، قرار است یک زبان تعریف شود و این به‌وسیله زبان دیگری موسوم به فرازبان، یعنی زبانی که همین جمله در آن است، انجام می‌شود. بنابراین باید در فرازبان از "چیزهایی" درباره عناصر این زبان سخن گفت. به‌عبارت‌دیگر، نیاز است تا در فرازبان از این "چیزها" نام برد و به آن‌ها رجوع کرد. می‌توان در فرازبان واژگان بنیادی زبان صوری را با قرار دادن آن‌ها درون جفت گیومه متمایز کرد.

بعلاوه نیاز است اشیائی را نام ببریم که گرچه در دامنه مصداقی مشخص هستند اما اشاره به مورد خاصی از این دامنه ندارند. مثل آنکه می‌خواهیم بگوییم «فرض کنید شئ‌ای یک عبارت LP باشد، ...» یا «اگر شئ‌ای عضو ƒLp باشد، آنگاه....». در این موارد به‌جای «شئ‌ای" از حروف کوچک الفبای یونانی به‌قرار β ،α ،γ و λ با اندیس و بی اندیس استفاده خواهیم کرد. به این‌ها، که درواقع عناصر فرازبان‌ هستند متغیرهای فرازبانی، گفته می‌شود.

اکنون ƒLp را تعریف می‌کنیم.

■ تعریف بازگشتی صورت

در گام یکم (I) عبارت‌های معینی از LP را صریحاً به عضویت ƒLp درمی‌آوریم. به این نحو که، می‌گوییم:

I: اتم‌ها و ثابت‌های منطقی عضو ƒLp هستند. (بنابراین ƒLp تهی نخواهد بود.)

در گام دوم (II) با یک الحاقی چهار قاعده‌ای به شرحی که خواهد آمد ƒLp را گسترش می‌دهیم (با این چهار قاعده، بر پایه عبارات تاکنون موجود، عبارات بیشتر برای ƒLp می‌سازیم). پس می‌گوییم؛

II.۱: اگر α عضو ƒLp باشد، آنگاه α~ نیز عضو ƒLp است.

مثال: بنا بر I، اتم p عضو ƒLp است و بنا بر II.۱ عبارت ~p نیز عضو ƒLp خواهد بود. و ازآنجاکه p~ عضو ƒLp است، مجدداً بنا بر II.۱ عبارت p~~ نیز عضو ƒLp است. (با تکرار روند II.۱ به هر تعداد دلخواه می‌توان برای ƒLp عضو ساخت.)

گام دوم را با وضع چهار قاعده دیگر تمام می‌کنیم و می‌گوییم:

اگر α و β عضو ƒLp باشند، آنگاه:

(α ∧ β) :II.۲
(α ∨ β) :II.۳
(α ⊃ β) :II.۴

عضو ƒLp هستند.

آنچه می‌ماند اینکه این تعریف هنوز نهایی نیست (جامع است ولی مانع نیست). یعنی، آیا عبارت‌های دیگر، غیر ازآنچه در این دو گام به عضویت ƒLp درآمده‌اند، هستند که عضو ƒLp باشند؟ پس، گام آخر (سوم) نهایی کردن (بستن) تعریف (وضع قوانین تألیف لفظ) است.

بنابراین، در گام سوم(III)، می‌گوییم:

فقط آن عبارات از LP عضو ƒLp هستند که به‌وسیله (I) و (II) ساخته‌شده باشند.

☚سه‌گانه بالا را قواعد نگارش LP می‌نامیم.
☚همیشه حرف آغازین اعضای ƒLp یک اتم یا "~" یا ")" است.

■ مثال: نگارش لفظ

نشان دهید عبارت‌های زیر عضو ƒLp هستند.

۱- β= (((p⊃q)∧(q∨ r))⊃(p∨r))⊃~(q∨s)))

۲- α= (~~ p⊃p)

حل ۱: با توجه به فهرست زیر، α عضو ƒLp است.

 
توجیه ساختعبارات ساخته
اتم‌ها عضو ƒLp هستند. (I)p۱.
۱ و II.۱.~p۲.
۲ و II.۱.~~p۳.
۳ و II.۴. (~~p⊃p)۴.
دنباله‌ای که عناصر آن عبارات ستون ۱ و به ترتیب از سطر ۱ تا ۴ است روند پیدایش (نگارش) اعضای ƒLp است. هر عضو این دنباله یک اتم است یا از عضوهای قبل بنا بر یک قاعده حاصل‌شده است. مراحل ۱ تا ۴ در بالا را می‌توان به‌صورت یک دنباله نشان داد:
≺p, ~p, ~~p, (~~p⊃p)≻

حل ۲: با توجه به فهرست زیر، β عضو ƒLp است.

 
توجیه ساختعبارات ساخته
 Ip۱.
 Iq۲.
 Ir۳.
 Is۴.
 ۱، ۲ و II(p⊃q)۵.
 ۲، ۳ و II(q∨r)۶.
 ۵، ۶ و II((p⊃q) ∧ (q∨r))۷.
 ۱، ۳ و II(p∨r)۸.
 ۲، ۴ و II(q∨s)۹.
 ۷، ۸ و II(((p⊃q)∧(q∨r)) ⊃(p∨r))۱۰.
 ۹ و II~(q∨s)۱۱.
 ۱۰، ۱۱ و II((((p⊃q)∧(q∨r)) ⊃(p∨r))⊃~(q ∨s))۱۲.
در زیر روند ۱ تا ۱۲ در بالا به‌صورت یک دنباله نشان داده‌شده:
≺ p, q, r, s, (p⊃q), (q ∨r), ((p⊃q)∧(q∨r)), (p∨r), (q∨s),
(((p⊃q)∧(q ∨r))⊃(p ∨r)), ~(q∨s),
((((p⊃q)∧(q∨r))⊃(p∨r)⊃~(q∨s)) ≻

■ فرمول‌ در منطق

زبان LP را می‌توان با معرفی عناصر جدید (برای مثال رابط‌ها و اتم‌ها از گونه‌های جدید) گسترش داد و زبان صوری بزرگ‌تری را ساخت. این همان چیزی است که در تئوری سورها (فصل 11 کتاب) رخ داد و اتم‌های «ثابت‌های انفرادی»، «حروف محمولی» و همچنین سه رابط «سور عمومی»، «سور وجودی» و «متغیر انفرادی» معرفی‌شده‌اند. در این زبان‌ها الفاظ تألیفی فقط "صورت‌های گزاره‌ای" آن‌گونه که در فصل‌ نه کتاب معرفی شدند نیستند، بلکه صورت‌های دیگر نیز به میان می‌آیند. منطق ‌دان‌ها به این صوَر «Well-Formed Formula» (با کوته‌سازی wff) می‌گویند. ازآنجاکه در متون ریاضی به زبان فارسی عباراتی مانند «Well Defined» و «Well Ordered» به ترتیب به «خوش-تعریف» و «خوش-ترتیب» برگردانده شده است، ما نیز به پیروی «پیکره / پیکرک(ها)ی خوش-ساخت» یا آسان‌تر فرمول خوش-ساخت را با همان کوته‌سازی، wff، بکار می‌بریم. و وقتی از زمینه مشخص است، فقط "فرمول" را ذکر می‌کنیم. مراد از "خوش-ساخت" نابسته بودن آن‌ها به هر تعبیری هستند که ممکن است به آن‌ها منتسب گردد. در یادداشت‌های بعد (صورت، تعبیر و معنا) دراین‌باره بیشتر می‌بینیم. حاصل کلام آنکه به عضوهای مجموعه ƒLp فرمول‌های (خوش-ساخت) LP می‌گوییم و فقط عضوهای این مجموعه را فرمول‌های ƒLp می‌نامیم.

■ فرمول شماتیک

به فرمولی که در آن حداقل یک متغیر فرازبانی به‌کاررفته، یک فرمول شماتیک گفته می‌شود. یک فرمول شماتیک معرفی تعداد نامتناهی فرمول است. برای مثال فرمول (p∨α) معرف (p∨(p∧q)) یا (p∨q) و مانند آن‌ها است.

■ فرمول اتمی

به یک فرمول غیر شماتیک که در آن رابطی بکار نرفته باشد فرمول اتمی و در غیر این صورت به آن فرمول غیر اتمی گفته می‌شود. بنابراین همه اتم‌ها فرمول اتمی هستند.

■ معرفی "≡":

"≡" را برای کوتاه نویسی (یک رابط تعریف‌شده) مطابق تعریف زیر به کارخواهیم برد:

α≡β ≝ (α ⊃ β) ∧ (β ⊃ α)

توجه داریم: "≡" یک نماد بنیادی زبان LP نیست، بلکه طبق تعریف در LP حاضر شده‌اند.

■ شمارایی مجموعه فرمول‌ها

• یادآوری از حساب (شماره گذاری گودل):

هر عدد طبیعی بزرگ‌تر از یک را به‌طور یکتا می‌توان به عوامل اول تجزیه کرد. به‌عبارت‌دیگر، برای هر n∈ℕ ؛n>۱ اعداد متمایز اول p۱, p۲ , . . . , pr [و فقط نیز آن‌ها] وجود دارند به قسمی که:

n=(p۱)a۱ × (p۲)a۲ × . . . × (pr)ar (ri∈ℕ; ri>۱); a۱∈ℕ ؛a۱>۰

برای مثال:

۱۶۵۲۹۹۴۰۸۶۴=۲۷×۳۱۷;
۱۰۰=۲۲×۵۲ ;
۶۳=۳۲×۷۱

و مانند آن‌ها.

حال تابع g را طوری تعریف می‌کنیم که به نماد‌های ابتدایی LP اعداد زیر را نظیر کند:

g(()=۱ , g())=۲, g(~)=۳ , g(∧)=۴, g(∨)=۵ , g(⊃)=۶ , g(p)=۷ , g(q)=۸ , g(r)=۹ , g(s)=۱۰ , g(t)=۱۱

سپس به هر عبارت در LP مانند e → c۱c۲...cm، عدد

۲g(c۱) × ۳g(c۲) × . . . × prg(cr)

را نظیر کرده به قسمی که در آن  ci حرف iام در e و امینr ،pr عدد اول باشد. برای مثال، برای عبارت (~∨~) داریم:

(~∨~) ↔ ۲۱×۳۳×۵۵×۷۳×۱۱۲ = ۷۰۰۳۶۳۱۲۵۰

به این ترتیب، یک رابطه ۱:۱ بین زیرمجمو‌عه‌ای از اعداد طبیعی و عبارات LP پدید می‌آید و ازاینجا مجموعه عبارات LP شمارا است؛ و چون مجموعه فرمول‌های LP، یعنی، ƒLp، زیرمجموعه عبارات آن است آنگاه ƒLp نیز شمارا است. اگر اتم‌های LP را نامتناهی و شمارا در نظر بگیریم، با توجه به نامتناهی بودن اعداد اول، هنوز ƒLp شمارا خواهد بود.

شمارایی ƒLp امکان برشمردن آن را میسر می‌سازد. به‌عبارت‌دیگر، می‌توان اعضای آن را به گونه زیر فهرست کرد:

α۱, α۲, α۳, . . . αk, . . .

به قسمی که هر عضو ƒLp در این فهرست باشد و هر αi یک عضو ƒLp باشد.

■ تصمیم پذیری فرمول خوش-ساخت در منطق گزاره‌ها

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

۱- اجرا الگوریتم برای هر مورد از مساله نوعی در زمان متناهی پایان می‌پذیرد.

۲- صحت الگوریتم، یعنی اجرای روند برای هر مورد از مساله نوعی منجر به جواب صحیح مسئله می‌گردد؛

در اینجا می‌خواهیم بدانیم آیا مسئله فرمول بودن در LC تصمیم پذیر است؟ به‌عبارت‌دیگر اگر ρ یک عبارت دلخواه LC و |ρ|>۰ باشد آنگاه الگوریتمی هست که ورودی آن ρ و خروجی آن پاسخ آری یا نه درباره فرمول بودن (خوش-ساخت بودن / به قاعده ساخته شده)  ρ باشد؟

برای مثال وقتی ورودی این الگوریتم هر یک از عبارات زیر باشد؛

۱- ((
۲- ((~p)
۳- )p(
۴- (p⊃((p⊃p)⊃(p⊃p)⊃(p⊃p))))

خروجی الگوریتم باید "نه" باشد؛ و برای ورودی‌های زیر و مانند آن‌ها؛

۱- (p⊃~q)
۲- p
۳- (p⊃((p⊃r)⊃((q•~p)⊃(p⊃s))))

باید "بله" باشد.

■ الگوریتمِ تصمیم پذیری فرمول

توجه: همزمان با ارائه الگوریتم، اجرای آن را برای:

ρ::(p⊃(~p⊃q))

پی خواهیم گرفت.

۰- z را اتمی می‌گیریم که در ρ نباشد؛ [مجموعه اتم‌ها را شمارش پذیر نامتناهی فرض کرده‌ایم و بعلاوه هر نماد در یک عبارت که پرانتز و رابط نباشد اتم خواهد بود.]

۱- z را جایگزین هر مورد اتم‌های ρ کرده و حاصل را A۱ نامیده. این عمل را  f۱ می‌نامیم. بنابراین:

A۱=f۱(ρ) =f۱((p⊃(~p⊃q)))=(z⊃(~z⊃z)

۲- z را جایگزین هر رویداد  ~z در A۱ کرده و حاصل را  A۲ نامیده. این عمل را  f۲ می‌نامیم. روشن است که: |A۲|≤|A۱|.

A۲ =f۲(A)=(z⊃(z⊃z))

۳- A۲ را از چپ به راست ‌کاویده و اولین زیرعبارت یافته در آن به شمای (zbz) را با z جایگزین کرده. حاصل را A۳ نامیده. روشن است که: |A۳|≤|A۲|. این عمل را  f۳ می‌نامیم.

A۳ =f۳(A۲)= (z⊃z)

۴- دستورالعمل ۲ و ۳ را به ترتیب (یعنی، f۳ºf۲ که آن را f۴ می‌نامیم) برای A۳ تکرار می‌کنیم و حاصل را  A۴ نامیده. این کار را تا جایی که، به فرض دربار nام، نتیجه به‌دست‌آمده روی An با خود An یکی شود، یا به‌عبارت‌دیگر داشته باشیم f۳ºf۲(An)=An ادامه می‌هیم. روشن است که در هر بار |An|<|An-۱| و دربار آخر |An+۱|=|An|.

A۴ =f۳ºf۲(A۳)=f۳ºf۲((z⊃z))=z
A۵ =f۳ºf۲(A۴)=A۴

۵- اگر An=z  آنگاه ρ فرمول و در غیر این صورت فرمول نیست.

چون برای n=۴ داریم: A۴ =z  پس ρ یعنی عبارت(p⊃(~p⊃q))  فرمول است.

توضیح: برای اثبات کارآمدی روند بالا (یعنی الگوریتم بودن آن) باید نشان داد اگر ρ فرمول باشد آنگاه عدد طبیعی n به قسمی که An=z وجود دارد (یعنی، اجرای الگوریتم در زمان محدود پایان می‌پذیرد که با توجه متناهی بودن طول عبارت ثابت می‌شود) و بعلاوه نیز نشان‌داد که اگر عدد طبیعی n به قسمی که An=z  باشد وجود داشته باشد آنگاه ρ فرمول است و در غیر این صورت ρ فرمول نیست (یعنی اثبات صحت الگوریتم، که این نیز یا توجه به خوانش یکتای فرمول اثبات می‌شود).

مثال بیشتر:

ρ :: (p⊃((p⊃p)⊃~(p⊃p)⊃(p⊃~p))))
A۱ =f۱(ρ)=(z⊃((z⊃z)⊃~(z⊃z)⊃(z⊃~z))))
A۲=f۲(A۱)=(z⊃((z⊃z)⊃~(z⊃z)⊃(z⊃z))))
A۳=f۳(A۲)=(z⊃(z⊃~(z⊃z)⊃(z⊃z))))
A۴=f۳(A۳)=(z⊃(z⊃~z⊃(z⊃z))))
A۵=f۲(A۴)=(z⊃(z⊃z⊃(z⊃z))))
A۶=f۳(A۵)=(z⊃(z⊃z⊃z)))
A۷=f۳ºf۲(A۶)=(z⊃(z⊃z⊃z)))=A۶
فرمول نیست. ρ پس A۶=A۷≠z چون

ρ :: (p⊃((p⊃~p)⊃(p • p)⊃(p∨~p))))
A۱=f۱(ρ)=(z⊃((z⊃~z)⊃((z • z)⊃(z∨~z))))

A۲=f۲(A۱)=(z⊃((z⊃z)⊃((z • z)⊃(z∨z))))
A۳= f۳(A۲)=(z⊃(z⊃((z • z)⊃(z∨z))))

A۴= f۴(A۳)=(z⊃(z⊃(z⊃(z∨z))))
A۵= f۴(A۴)=(z⊃(z⊃(z⊃z)))
A۶= f۴(A۵)=(z⊃(z⊃z))
A۷= f۴(A۶)=(z⊃z)
A۸=f۴(A۷)=z
A۹=f۴(A۸)=A۸
فرمول است. ρ پس A۸=A۹=z چون

■  درخت پیکربندی فرمول:

در این بند به نگارش و خوانش فرمول (wff) در یک ساختار درختی (نمودار درختی) می‌پردازیم. به چنین ساختاری درخت پیکربندی (یا درخت فراکافت - Parse tree) گفته می‌شود. فرض می‌کنیم α فرمول باشد. درخت پیکربندی α یا Treeα -  را به گونه بازگشتی مطابق زیر تعریف می‌کنیم:

آ- اگر  α اتمی باشد آنگاه؛

Treeα=۰ α

ب- اگر α به شمای ~β باشد آنگاه؛

شمای فرمول در منطقTreeα=

ج- اگر  α به شمای (γbλ)  باشد آنگاه؛

شمای فرمول در منطقTree (γbλ)=

■ مثال برای درخت پیکربندی

درخت فراکافت (تجزیه) در منطق

درخت فراکافت (تجزیه) در منطق

☚

فرض کنید α یک فرمول و  Treeα درخت پیکربندی آن باشد، آنگاه محتوی هر گره‌ Treeα یک زیرفرمول α است و بعلاوه محتوی هر گره تالی زیرفرمول-بی‌واسطه گره مقدم خود است.

■ شناسایی درخت فراکافت (Parse tree)

فرض کنید T یک درخت دودویی باشد به‌گونه‌ای که؛

۱-  محتوی هر برگ(گره انتهایی) یک اتم باشد؛

۲- محتوی هر گره ساده T یک فرمول به شمای ~β بوده و بعلاوه فرزند این گره دارای محتوی β باشد؛

۳- محتوی هر گره انشعاب در T فرمولی به شمای (γbλ) بوده و بعلاوه فرزندان چپ و راست این گره به ترتیب دارای محتوی γ و λ باشد؛

در این صورت به T یک درخت پیکربندی می‌گوییم. می‌توان نشان داد که T متناظر با درخت پیکربندی فرمولی است که محتوای ریشه T است.

درخت تحلیل فرمول منطق

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

◄ توجه: