Қысқартылған бөліну: Логикалық дәлелдеу әдісі мен "D" белгілемесі
Condensed detachment
Конденсатты бөлу (Rule D) – екі логикалық тұжырымнан ең жалпы қорытынды шығару әдісі. Кальюман дәлелдегендей, бұл әдіс модас поненс және субституциясы бар кез келген логика жүйесінде қолданылады.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Конденсацияланған ажырату (D ережесі) – екі формалды логикалық тұжырымдаманы ескере отырып, ең жалпы қорытындыны табу әдісі. Оны 1950 жылдары ирланд логигі Кареу Мередит әзірледі және ол Łukasiewicz еңбектерінен шабыттанды. Дж. А. Калман мынаны дәлелдеді: біркелкі алмастыру (көрсеткіштің барлық мысалдары бірдей мазмұнмен алмастырылады) және modus ponens қадамдарының тізбегі арқылы алынған кез келген қорытындыны, конденсацияланған ажыратудың өзі ғана шығара алады, немесе конденсацияланған ажыратудың өзі ғана шығара алатын нәрсенің алмастыру мысалы болып табылады. Бұл конденсацияланған ажыратуды, D-толық немесе толық емес екеніне қарамастан, modus ponens және алмастыру қағидаларына ие кез келген логикалық жүйе үшін пайдалы етеді.
Condensed detachment (Rule D) is a method of finding the most general possible conclusion given two formal logical statements. It was developed by the Irish logician Carew Meredith in the 1950s and inspired by the work of Łukasiewicz. J. A. Kalman proved that any conclusion that can be generated by a sequence of uniform substitution (all instances of a variable are replaced with the same content) and modus ponens steps can either be generated by condensed detachment alone, or is a substitution instance of something that can be generated by condensed detachment alone. This makes condensed detachment useful for any logic system that has modus ponens and substitution, regardless of whether or not it is D complete.
D-белгісі
Берілген негізгі және кішігірім жорамалдар нақты бір қорытындыны анықтайтынын (айнымалылардың атауын өзгертуден басқа), Мередит екі ғана мәлімдемені көрсету жеткілікті екенін және қысқартылған ажыратуды қосымша белгілерсіз қолдануға болатынын атап өтті. Бұл дәлелдемелерді жазу үшін "D белгілеуіне" әкелді. Бұл белгілеуде "D" операторы қысқартылған ажыратуды білдіреді және стандартты префикс түрінде 2 аргумент қабылдайды. Мысалы, егер сізде төрт аксиома болса, D белгілеуімен жазылған үлгілі дәлел мынадай болуы мүмкін: DD12D34, бұл екі бұрынғы қысқартылған ажырату қадамдарының нәтижесін пайдаланып, қысқартылған ажырату қадамын көрсетеді, олардың біріншісі 1 және 2 аксиомаларын, ал екіншісі 3 және 4 аксиомаларын қолданды. Бұл белгілеу, кейбір автоматтандырылған теорема дәлелдеушілерде қолданылудан басқа, кейде дәлелдемелердің тізімдерінде де кездеседі. Мысалы, Metamath жобасының mmsolitaire-дегі "ең қысқа дәлелдемелер" дерекқоры мұндай дәлелдемелермен 196 теореманы қамтиды. Қысқартылған ажыратудың біріктіруді қолдануы 1965 жылы ұсынылған автоматтандырылған теоремаларды дәлелдеудің шешім әдісінен бұрын пайда болды.
Since a given major premise and a given minor premise uniquely determine the conclusion (up to variable renaming), Meredith observed that it was only necessary to note which two statements were involved and that the condensed detachment can be used without any other notation required. This led to the "D notation" for proofs. This notation uses the "D" operator to mean condensed detachment, and takes 2 arguments, in a standard prefix notation string. For example, if you have four axioms a typical proof in D notation might look like: DD12D34 which shows a condensed detachment step using the result of two prior condensed detachment steps, the first of which used axioms 1 and 2, and the second of which used axioms 3 and 4. This notation, besides being used in some automated theorem provers, sometimes appears in catalogs of proofs. For example, the "shortest known proofs" database of Metamath's mmsolitaire project features 196 theorems with such proofs. Condensed detachment's use of unification predates the resolution technique of automated theorem proving which was introduced in 1965.
Артықшылықтар
Автоматтандырылған теореманы дәлелдеу үшін конденсациялық ажырату, қарапайым modus ponens және біркелкі алмастырудан бірнеше артықшылықтарға ие. Modus Ponens және алмастыру арқылы дәлелдеу кезінде айнымалыларды алмастыру үшін шексіз көп мүмкіндіктер болады. Бұл, келесі қадамдардың саны да шексіз дегенді білдіреді. Ал конденсациялық ажыратуда дәлелдеудегі келесі қадамдардың саны шектеулі. Толық конденсациялық ажырату дәлелдерін белгілеу үшін қолданылатын D нотациясы, оларды каталогтау және іздеу мақсатында оңай сипаттауға мүмкіндік береді. Типикалық толық 30 қадамдық дәлелдеу D нотациясында 60 символдан кем болады (аксиомалардың тұжырымын есептемегенде).
For automated theorem proving condensed detachment has a number of advantages over raw modus ponens and uniform substitution. At a Modus Ponens and substitution proof you have an infinite number of choices for what you can substitute for variables. This means that you have an infinite number of possible next steps. With condensed detachment there are only a finite number of possible next steps in a proof. The D notation for complete condensed detachment proofs allows easy description of proofs for cataloging and search. A typical complete 30 step proof is less than 60 characters long in D notation (excluding the statement of the axioms.)