This site is not complete. The work to converting the volumes of സര്‍വ്വവിജ്ഞാനകോശം is on progress. Please bear with us
Please contact webmastersiep@yahoo.com for any queries regarding this website.
Reading Problems? see Enabling Malayalam
തിയറം പ്രൂവിങ്
സര്‍വ്വവിജ്ഞാനകോശം സംരംഭത്തില്‍ നിന്ന്
(New page: തിയറം പ്രൂവിങ് ഠവലീൃലാ ുൃീ്ശിഴ ഗണിതം, എഐ (ആര്‍ട്ടിഫിഷ്യല്‍ ഇന്റലിജന...) |
|||
| വരി 1: | വരി 1: | ||
| - | തിയറം പ്രൂവിങ് | + | =തിയറം പ്രൂവിങ് = |
| + | Theorem proving | ||
| - | + | ഗണിതം, എഐ (ആര്‍ട്ടിഫിഷ്യല്‍ ഇന്റലിജന്‍സ്) തുടങ്ങിയ വിജ്ഞാന ശാഖകളിലെ പ്രമേയങ്ങളെ തെളിയിക്കുകയോ അതിനാവശ്യമായ പ്രതിവിധികള്‍ നിര്‍ദേശിക്കുകയോ ചെയ്യുക, സോഫ്റ്റ് വെയര്‍ - ഹാര്‍ഡ് വെയര്‍ സിസ്റ്റങ്ങളെ വിശകലന രീത്യാ വിലയിരുത്തുക എന്നിവയ്ക്കായി കംപ്യൂട്ടര്‍ പ്രോഗ്രാമുകള്‍ പ്രയോജനപ്പെടുത്തുന്ന പ്രക്രിയ. സ്വചാലിത തിയറം പ്രൂവിങ് രണ്ട് തരത്തിലാണ് നടക്കുന്നത്: പ്രമേയങ്ങളെ തെളിയിക്കുക മാത്രം ചെയ്യുക; തന്നിരിക്കുന്ന അഭിഗൃഹീതങ്ങള്‍ (axioms) അടിസ്ഥാനമാക്കി ഏതെല്ലാം നിഗമനങ്ങളിലെത്താനാകുമെന്നും അവയില്‍ ഗണിത രീത്യാ ഉപപത്തിമത്തായവ ഏതൊക്കെയാണെന്നും കണ്ടുപിടിക്കുക. | |
| - | + | തിയറം പ്രൂവിങ്ങിനുള്ള ആദ്യത്തെ കംപ്യൂട്ടര്‍ പ്രോഗ്രാം 1957-ലാണ് എഴുതപ്പെട്ടത്. ബൂളിയന്‍ ബീജഗണിതത്തിലെ പ്രമേയങ്ങള്‍ക്ക് ഉപപത്തി നിര്‍ദേശിക്കുവാന്‍ അലന്‍ ന്യൂവെല്‍, ജെ.സി. ഷാ, ഹെര്‍ബെര്‍ട്ട് സൈമണ്‍ എന്നിവര്‍ ചേര്‍ന്ന് ലോജിക്ക് തിയറിസ്റ്റ് (എല്‍ടി) എന്ന പ്രോഗ്രാം തയ്യാറാക്കി. തുടര്‍ന്ന് ജ്യാമിതിയിലെ പ്രമേയങ്ങള്‍, ഗ്രൂപ്പ് തിയറി, സ്ട്രിങ് സേര്‍ച്ചിങ് അല്‍ഗോരിഥം എന്നീ മേഖലകളിലും പ്രോഗ്രാമുകള്‍ പ്രയോഗത്തില്‍ വന്നു. | |
| - | + | തിയറം പ്രൂവിങ് പ്രോഗ്രാമുകളെ പ്രധാനമായി രണ്ടായി വര്‍ഗീകരിക്കാം: പ്രഥമ പ്രകാര ഉപപത്തി (first order logic) അടിസ്ഥാനമാക്കിയുള്ളവയും ഉച്ചസ്ഥായി ഉപപത്തികളെ (higher order logic) അടിസ്ഥാനമാക്കിയുള്ളവയും. | |
| - | + | '''പ്രഥമപ്രകാര ഉപപത്തി രീതി.''' പ്രമേയം ഉള്‍ക്കൊള്ളുന്നവയില്‍ ഏതാനും ചരങ്ങള്‍ക്ക് സ്ഥിര മൂല്യങ്ങള്‍ കല്പിച്ച് അതിലൂടെ പ്രമേയം തെളിയിക്കപ്പെട്ടോ എന്ന് പരിശോധിക്കുന്നു; ആവശ്യമെങ്കില്‍ കൂടുതല്‍ ചരങ്ങള്‍ക്ക് സ്ഥിര മൂല്യങ്ങള്‍ കല്പിച്ച് പരിശോധന ആവര്‍ത്തിക്കുകയുമാവാം. ആദ്യകാലത്തെ തിയറം പ്രൂവിങ് പ്രോഗ്രാമുകള്‍ പ്രവര്‍ത്തിച്ചിരുന്നത് ഈ രീതിയിലാണ്. തുടര്‍ന്ന് 'റെസൊല്യൂഷെന്‍ തത്ത്വം' ആവിഷ്ക്കരിക്കപ്പെട്ടു. തന്നിരിക്കുന്ന രണ്ട് പ്രസ്താവനകളെ (statements) അടിസ്ഥാനമാക്കി ആദ്യം പൊതുവായ ഒരു നിഗമനം കണ്ടെത്തുന്നു. പ്രമേയത്തിന്റെ വിപരീതം ശരിയാണെന്ന നിഗമനത്തോടെ ക്രിയ ചെയ്ത് പരസ്പരം വിരുദ്ധവും യുക്തിരഹിതവുമായ നിര്‍ണയനയത്തിലെത്തുന്നതോടെ, പ്രമേയത്തിനു വിപരീതമായ ഏതു നിഗമനവും തെറ്റാണെന്നു തെളിയുന്നു; ഇതോടെ പ്രമേയത്തിന്റെ യുക്തി ഭദ്രത തെളിയിക്കപ്പെടുന്നു. ഈ തരത്തിലുള്ള 'നെഗേഷന് സമീപനം' മിക്കപ്പോഴും ഫലവത്താകാം. തന്നിരിക്കുന്ന പ്രസ്താവനകളിലെ ഏതു ജോഡിയാണ് നെഗേഷനുവേണ്ടി തിരഞ്ഞെടുക്കേണ്ടത് എന്നു തീരുമാനിക്കുന്നത് ഒരു നിശ്ചിത അല്‍ഗോരിഥത്തിലൂടെയായിരിക്കും. പ്രസ്തുത അല്‍ഗോരിഥത്തിന്റെ ശേഷിക്കനുസൃതമായി റെസൊല്യൂഷന്‍ രീതിയുടെ ദക്ഷത വ്യത്യാസപ്പെടാം. ഇന്‍പുട്ട് പ്രസ്താവനകളുടെ ഘടനാപര വിശകലനത്തിലൂടെ നെഗേഷന് അനുയോജ്യമായ ജോഡികളെ കണ്ടെത്തി, അവയ്ക്കിടയിലെ അന്യോന്യബന്ധം സ്ഥാപിക്കുകയാണ് ഇതിനുള്ള ഒരു പോംവഴി; മെട്രിക്സ് രീതികളിലൂടെയും പ്രശ്ന പരിഹാരം കണ്ടെത്താനാകും. ബൂളിയന്‍ ഉപസൂത്രങ്ങളാല്‍ ഒരു മെട്രിക്സ് രൂപപ്പെടുത്താവുന്ന വിധത്തില്‍ പ്രമേയത്തിന്റെ നെഗേഷനെ 'നോര്‍മലൈസ്' ചെയ്യുകയാണ് ആദ്യപടി. തുടര്‍ന്ന് ചരങ്ങള്‍ക്കു മൂല്യം കല്പിക്കുന്നതിലൂടെ ലഭിക്കുന്ന ഓരോ മെട്രിക്സ് പഥവും വൈരുധ്യത്തിലെത്തുന്നുവെന്നു സമര്‍ഥിക്കുന്നതോടെ പ്രമേയം തെളിയിക്കപ്പെട്ടതായി കരുതാനാകും. ടാബ്ളോ രീതിയാണ് മറ്റൊരു സമീപനം. ഇന്‍പുട്ട് സൂത്രത്തില്‍ നിന്ന് ഒന്നിലധികം പ്രസാര നിയമങ്ങളിലൂടെ (expansion rules) ഒരു 'ട്രീ'ക്ക് രൂപം നല്കി, ട്രീയിലെ എല്ലാ പഥങ്ങളിലും വൈരുധ്യമുണ്ടെന്നു തെളിയിച്ച്, പ്രമേയം സാധുവാക്കുന്നു. എന്നാല്‍ ഈ പദങ്ങളെല്ലാം 'മിനിമലോ, (minimal) 'ഡിസ്ജോയിന്റോ' (disjoint) ആയിരിക്കണമെന്നില്ല എന്നതാണ് ഈ രീതിയുടെ പേരായ്മ. 'മോഡല്‍ ജനറേഷന്‍'രീതിയില്‍ തയ്യാറാക്കപ്പെടുന്ന പഥങ്ങള്‍, മൊത്തത്തില്‍ 'മിനിമല്‍'ആയിരിക്കും. ഇവ ടാബ്ളോ രീതിയേക്കാള്‍ മെച്ചപ്പെട്ടവയാണ്. | |
| - | + | '''ഉച്ചസ്ഥായി ഉപപത്തി പ്രോഗ്രാമുകള്‍.''' ഹാര്‍ഡ് വെയര്‍, സോഫ്റ്റ് വെയര്‍, പ്രോട്ടോകോള്‍ പരിശോധന, കംപ്യൂട്ടര്‍ സുരക്ഷ എന്നിവയ്ക്ക് ഈ രീതിയാണ് ഉപയോഗിക്കുന്നത്. ആദ്യമായി സിസ്റ്റത്തിന്റെ കാര്യനിര്‍വഹണ ക്ഷമത തിട്ടപ്പെടുത്തി, അതിന്റെ സ്റ്റേറ്റ് ട്രാന്‍സിഷന്‍ ഡയഗ്രം പഠന വിധേയമാക്കുന്നു. തുടര്‍ന്ന് ഈ അവസ്ഥയില്‍ പ്രസ്തുത പ്രമേയം നിലനില്ക്കാവുന്നതാണോ എന്ന് 'മോഡല്‍ ചെക്കറുകളിലൂടെ'പരിശോധിക്കുന്നു. മോഡല്‍ ചെക്കറുകളില്‍ ഏറ്റവും പ്രയോഗക്ഷമമാണ് 1993-ല്‍ മക്മില്ലന്‍ രൂപപ്പെടുത്തിയ എസ്എംവി (സിംബോളിക് മോഡല്‍ വെരിഫയര്‍). 10100-ല്‍ കൂടുതല്‍ അവസ്ഥകളുള്ള ബൃഹത് സിസ്റ്റങ്ങളെ വിലയിരുത്താന്‍ എസ്എംവി ഉപയോഗിക്കപ്പെട്ടിട്ടുണ്ട്. IEEE (Institute of Electrical and Electronic Engineers) ഫ്യൂച്ചെര്‍ബസ് പ്രോട്ടോകോളിന്റെ ന്യൂനതകള്‍ കണ്ടെത്താന്‍ സഹായിച്ചതും എസ്എംവിയാണ്. ഉപയോക്താവിന്റെ നിര്‍ദേശാനുസരണം തിയറം പ്രൂവിങ് പ്രോഗ്രാമുകള്‍ സജ്ജീകരിക്കാന്‍ സൗകര്യമുള്ള രണ്ട് ഉച്ചസ്ഥായി ഉപപത്തി രീതികളാണ് എച്ച്ഒഎല്‍ (ഹയര്‍ ഓര്‍ഡര്‍ ലോജിക്), പിവിഎസ് (പ്രോട്ടോടൈപ്പ് വെരിഫിക്കേഷന്‍ സിസ്റ്റം) എന്നിവ. സുരക്ഷാ ആവശ്യങ്ങള്‍ക്കായി തയ്യാറാക്കപ്പെട്ട ഹാര്‍ഡ് വെയര്‍, അല്‍ഗോരിഥം തുടങ്ങിയവയെ വിലയിരുത്തുക; മൈക്രോപ്രോസസ്സര്‍ ഉള്‍പ്പെടെയുള്ള കംപ്യൂട്ടര്‍ സിസ്റ്റങ്ങളെ അപഗ്രഥിക്കുക, ഹരണക്രിയ നടത്തുന്ന അല്‍ഗോരിഥങ്ങളെ പരിശോധിക്കുക എന്നിവയ്ക്കായിട്ടാണ് ഇവ പ്രയോജനപ്പെടുത്തുന്നത്. | |
| - | + | ||
| - | + | ||
Current revision as of 09:45, 1 ജൂലൈ 2008
തിയറം പ്രൂവിങ്
Theorem proving
ഗണിതം, എഐ (ആര്‍ട്ടിഫിഷ്യല്‍ ഇന്റലിജന്‍സ്) തുടങ്ങിയ വിജ്ഞാന ശാഖകളിലെ പ്രമേയങ്ങളെ തെളിയിക്കുകയോ അതിനാവശ്യമായ പ്രതിവിധികള്‍ നിര്‍ദേശിക്കുകയോ ചെയ്യുക, സോഫ്റ്റ് വെയര്‍ - ഹാര്‍ഡ് വെയര്‍ സിസ്റ്റങ്ങളെ വിശകലന രീത്യാ വിലയിരുത്തുക എന്നിവയ്ക്കായി കംപ്യൂട്ടര്‍ പ്രോഗ്രാമുകള്‍ പ്രയോജനപ്പെടുത്തുന്ന പ്രക്രിയ. സ്വചാലിത തിയറം പ്രൂവിങ് രണ്ട് തരത്തിലാണ് നടക്കുന്നത്: പ്രമേയങ്ങളെ തെളിയിക്കുക മാത്രം ചെയ്യുക; തന്നിരിക്കുന്ന അഭിഗൃഹീതങ്ങള്‍ (axioms) അടിസ്ഥാനമാക്കി ഏതെല്ലാം നിഗമനങ്ങളിലെത്താനാകുമെന്നും അവയില്‍ ഗണിത രീത്യാ ഉപപത്തിമത്തായവ ഏതൊക്കെയാണെന്നും കണ്ടുപിടിക്കുക.
തിയറം പ്രൂവിങ്ങിനുള്ള ആദ്യത്തെ കംപ്യൂട്ടര്‍ പ്രോഗ്രാം 1957-ലാണ് എഴുതപ്പെട്ടത്. ബൂളിയന്‍ ബീജഗണിതത്തിലെ പ്രമേയങ്ങള്‍ക്ക് ഉപപത്തി നിര്‍ദേശിക്കുവാന്‍ അലന്‍ ന്യൂവെല്‍, ജെ.സി. ഷാ, ഹെര്‍ബെര്‍ട്ട് സൈമണ്‍ എന്നിവര്‍ ചേര്‍ന്ന് ലോജിക്ക് തിയറിസ്റ്റ് (എല്‍ടി) എന്ന പ്രോഗ്രാം തയ്യാറാക്കി. തുടര്‍ന്ന് ജ്യാമിതിയിലെ പ്രമേയങ്ങള്‍, ഗ്രൂപ്പ് തിയറി, സ്ട്രിങ് സേര്‍ച്ചിങ് അല്‍ഗോരിഥം എന്നീ മേഖലകളിലും പ്രോഗ്രാമുകള്‍ പ്രയോഗത്തില്‍ വന്നു.
തിയറം പ്രൂവിങ് പ്രോഗ്രാമുകളെ പ്രധാനമായി രണ്ടായി വര്‍ഗീകരിക്കാം: പ്രഥമ പ്രകാര ഉപപത്തി (first order logic) അടിസ്ഥാനമാക്കിയുള്ളവയും ഉച്ചസ്ഥായി ഉപപത്തികളെ (higher order logic) അടിസ്ഥാനമാക്കിയുള്ളവയും.
പ്രഥമപ്രകാര ഉപപത്തി രീതി. പ്രമേയം ഉള്‍ക്കൊള്ളുന്നവയില്‍ ഏതാനും ചരങ്ങള്‍ക്ക് സ്ഥിര മൂല്യങ്ങള്‍ കല്പിച്ച് അതിലൂടെ പ്രമേയം തെളിയിക്കപ്പെട്ടോ എന്ന് പരിശോധിക്കുന്നു; ആവശ്യമെങ്കില്‍ കൂടുതല്‍ ചരങ്ങള്‍ക്ക് സ്ഥിര മൂല്യങ്ങള്‍ കല്പിച്ച് പരിശോധന ആവര്‍ത്തിക്കുകയുമാവാം. ആദ്യകാലത്തെ തിയറം പ്രൂവിങ് പ്രോഗ്രാമുകള്‍ പ്രവര്‍ത്തിച്ചിരുന്നത് ഈ രീതിയിലാണ്. തുടര്‍ന്ന് 'റെസൊല്യൂഷെന്‍ തത്ത്വം' ആവിഷ്ക്കരിക്കപ്പെട്ടു. തന്നിരിക്കുന്ന രണ്ട് പ്രസ്താവനകളെ (statements) അടിസ്ഥാനമാക്കി ആദ്യം പൊതുവായ ഒരു നിഗമനം കണ്ടെത്തുന്നു. പ്രമേയത്തിന്റെ വിപരീതം ശരിയാണെന്ന നിഗമനത്തോടെ ക്രിയ ചെയ്ത് പരസ്പരം വിരുദ്ധവും യുക്തിരഹിതവുമായ നിര്‍ണയനയത്തിലെത്തുന്നതോടെ, പ്രമേയത്തിനു വിപരീതമായ ഏതു നിഗമനവും തെറ്റാണെന്നു തെളിയുന്നു; ഇതോടെ പ്രമേയത്തിന്റെ യുക്തി ഭദ്രത തെളിയിക്കപ്പെടുന്നു. ഈ തരത്തിലുള്ള 'നെഗേഷന് സമീപനം' മിക്കപ്പോഴും ഫലവത്താകാം. തന്നിരിക്കുന്ന പ്രസ്താവനകളിലെ ഏതു ജോഡിയാണ് നെഗേഷനുവേണ്ടി തിരഞ്ഞെടുക്കേണ്ടത് എന്നു തീരുമാനിക്കുന്നത് ഒരു നിശ്ചിത അല്‍ഗോരിഥത്തിലൂടെയായിരിക്കും. പ്രസ്തുത അല്‍ഗോരിഥത്തിന്റെ ശേഷിക്കനുസൃതമായി റെസൊല്യൂഷന്‍ രീതിയുടെ ദക്ഷത വ്യത്യാസപ്പെടാം. ഇന്‍പുട്ട് പ്രസ്താവനകളുടെ ഘടനാപര വിശകലനത്തിലൂടെ നെഗേഷന് അനുയോജ്യമായ ജോഡികളെ കണ്ടെത്തി, അവയ്ക്കിടയിലെ അന്യോന്യബന്ധം സ്ഥാപിക്കുകയാണ് ഇതിനുള്ള ഒരു പോംവഴി; മെട്രിക്സ് രീതികളിലൂടെയും പ്രശ്ന പരിഹാരം കണ്ടെത്താനാകും. ബൂളിയന്‍ ഉപസൂത്രങ്ങളാല്‍ ഒരു മെട്രിക്സ് രൂപപ്പെടുത്താവുന്ന വിധത്തില്‍ പ്രമേയത്തിന്റെ നെഗേഷനെ 'നോര്‍മലൈസ്' ചെയ്യുകയാണ് ആദ്യപടി. തുടര്‍ന്ന് ചരങ്ങള്‍ക്കു മൂല്യം കല്പിക്കുന്നതിലൂടെ ലഭിക്കുന്ന ഓരോ മെട്രിക്സ് പഥവും വൈരുധ്യത്തിലെത്തുന്നുവെന്നു സമര്‍ഥിക്കുന്നതോടെ പ്രമേയം തെളിയിക്കപ്പെട്ടതായി കരുതാനാകും. ടാബ്ളോ രീതിയാണ് മറ്റൊരു സമീപനം. ഇന്‍പുട്ട് സൂത്രത്തില്‍ നിന്ന് ഒന്നിലധികം പ്രസാര നിയമങ്ങളിലൂടെ (expansion rules) ഒരു 'ട്രീ'ക്ക് രൂപം നല്കി, ട്രീയിലെ എല്ലാ പഥങ്ങളിലും വൈരുധ്യമുണ്ടെന്നു തെളിയിച്ച്, പ്രമേയം സാധുവാക്കുന്നു. എന്നാല്‍ ഈ പദങ്ങളെല്ലാം 'മിനിമലോ, (minimal) 'ഡിസ്ജോയിന്റോ' (disjoint) ആയിരിക്കണമെന്നില്ല എന്നതാണ് ഈ രീതിയുടെ പേരായ്മ. 'മോഡല്‍ ജനറേഷന്‍'രീതിയില്‍ തയ്യാറാക്കപ്പെടുന്ന പഥങ്ങള്‍, മൊത്തത്തില്‍ 'മിനിമല്‍'ആയിരിക്കും. ഇവ ടാബ്ളോ രീതിയേക്കാള്‍ മെച്ചപ്പെട്ടവയാണ്.
ഉച്ചസ്ഥായി ഉപപത്തി പ്രോഗ്രാമുകള്‍. ഹാര്‍ഡ് വെയര്‍, സോഫ്റ്റ് വെയര്‍, പ്രോട്ടോകോള്‍ പരിശോധന, കംപ്യൂട്ടര്‍ സുരക്ഷ എന്നിവയ്ക്ക് ഈ രീതിയാണ് ഉപയോഗിക്കുന്നത്. ആദ്യമായി സിസ്റ്റത്തിന്റെ കാര്യനിര്‍വഹണ ക്ഷമത തിട്ടപ്പെടുത്തി, അതിന്റെ സ്റ്റേറ്റ് ട്രാന്‍സിഷന്‍ ഡയഗ്രം പഠന വിധേയമാക്കുന്നു. തുടര്‍ന്ന് ഈ അവസ്ഥയില്‍ പ്രസ്തുത പ്രമേയം നിലനില്ക്കാവുന്നതാണോ എന്ന് 'മോഡല്‍ ചെക്കറുകളിലൂടെ'പരിശോധിക്കുന്നു. മോഡല്‍ ചെക്കറുകളില്‍ ഏറ്റവും പ്രയോഗക്ഷമമാണ് 1993-ല്‍ മക്മില്ലന്‍ രൂപപ്പെടുത്തിയ എസ്എംവി (സിംബോളിക് മോഡല്‍ വെരിഫയര്‍). 10100-ല്‍ കൂടുതല്‍ അവസ്ഥകളുള്ള ബൃഹത് സിസ്റ്റങ്ങളെ വിലയിരുത്താന്‍ എസ്എംവി ഉപയോഗിക്കപ്പെട്ടിട്ടുണ്ട്. IEEE (Institute of Electrical and Electronic Engineers) ഫ്യൂച്ചെര്‍ബസ് പ്രോട്ടോകോളിന്റെ ന്യൂനതകള്‍ കണ്ടെത്താന്‍ സഹായിച്ചതും എസ്എംവിയാണ്. ഉപയോക്താവിന്റെ നിര്‍ദേശാനുസരണം തിയറം പ്രൂവിങ് പ്രോഗ്രാമുകള്‍ സജ്ജീകരിക്കാന്‍ സൗകര്യമുള്ള രണ്ട് ഉച്ചസ്ഥായി ഉപപത്തി രീതികളാണ് എച്ച്ഒഎല്‍ (ഹയര്‍ ഓര്‍ഡര്‍ ലോജിക്), പിവിഎസ് (പ്രോട്ടോടൈപ്പ് വെരിഫിക്കേഷന്‍ സിസ്റ്റം) എന്നിവ. സുരക്ഷാ ആവശ്യങ്ങള്‍ക്കായി തയ്യാറാക്കപ്പെട്ട ഹാര്‍ഡ് വെയര്‍, അല്‍ഗോരിഥം തുടങ്ങിയവയെ വിലയിരുത്തുക; മൈക്രോപ്രോസസ്സര്‍ ഉള്‍പ്പെടെയുള്ള കംപ്യൂട്ടര്‍ സിസ്റ്റങ്ങളെ അപഗ്രഥിക്കുക, ഹരണക്രിയ നടത്തുന്ന അല്‍ഗോരിഥങ്ങളെ പരിശോധിക്കുക എന്നിവയ്ക്കായിട്ടാണ് ഇവ പ്രയോജനപ്പെടുത്തുന്നത്.
