CARINE: Бірінші реттік логикалық дәлелдеуші және кешіктірілген клауза құрастыру стратегиясы
CARINE
CARINE – бірінші реттік логикалық теореманы автоматты түрде дәлелдейтін жүйе. DCC және ATS стратегияларын қолданып, іздеуді жетілдіреді. Теорема дәлелдеуге арналған.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
CARINE (Computer Aided Reasoning Engine) – бірінші реттік классикалық логикалық автоматтандырылған теореманы дәлелдеуші. Ол бастапқыда тереңдікке бірінші іздеу алгоритміне негізделген стратегиялардың – кешіктірілген клауза құрылымының (DCC) және атрибуттар тізбегінің (ATS) – жақсарту әсерін зерттеу үшін құрылды. CARINE-нің негізгі іздеу алгоритмі – жартылай сызықтық ажыратылым (SLR), ол итеративті тереңдету арқылы тереңдікке бірінші іздеу (тереңдіктегі итеративті тереңдету (DFID) деп те аталады) негізінде құрылған және THEO сияқты теореманы дәлелдеушілерде қолданылады. SLR жоғары дедуктивтік жылдамдыққа қол жеткізу үшін DCC-ді, ал іздеу кеңістігін қысқарту үшін ATS-ті пайдаланады.
CARINE (Computer Aided Reasoning Engine) is a first order classical logic automated theorem prover. It was initially built for the study of the enhancement effects of the strategies delayed clause construction (DCC) and attribute sequences (ATS) in a depth first search based algorithm. CARINE's main search algorithm is semi linear resolution (SLR) which is based on an iteratively deepening depth first search (also known as depth first iterative deepening (DFID)) and used in theorem provers like THEO. SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space.
Келесіге сәйкес нысанды құру
Кейінге қалдырылатын шарт құрастыру – бұл теореманы дәлелдеушінің өнімділігін арттыратын, шарттарды құрастыруға жұмсалатын жұмысты ең төменгі деңгейге дейін азайтатын стратегия. Қолданылған тұжырымдамалық ереженің әрбір қорытындысын (шартын) құрастырудың орнына, теореманы дәлелдеуші осы шартты тастауға немесе құрастыруға шешім қабылдағанға дейін оны құрастыру туралы ақпарат уақытша сақталады. Егер теореманы дәлелдеуші шартты сақтауға шешім қабылдаса, ол жадқа сақталады, әйтпесе шартты құрастыруға арналған ақпарат жойылады. Шығарылған шартты құрастыруға болатын ақпаратты сақтау үшін дерлік қосымша процессор операциялары қажет емес. Дегенмен, шартты құрастыру көп уақытты алуы мүмкін. Кейбір теореманы дәлелдеушілер жалпы орындалу уақытының 30-40% құрастыруға және шарттарды жоюға жұмсайды. Кейінге қалдырылатын шарт құрастыру арқылы осы ысырап болған уақытты үнемдеуге болады. Кейінге қалдырылатын шарт құрастыру, әсіресе бірінші реттік шарттар сияқты, қысқа мерзім ішінде көптеген аралық шарттар құрастырылып, жойылған кезде өте пайдалы, себебі мұндай қысқа өмір сүретін шарттарды құрастыруға жұмсалатын операциялар орындалмайды. Кейінге қалдырылатын шарт құрастыру тек қана логикалық шарттармен шешілетін теоремалар үшін тиімді болмауы мүмкін.
Delayed Clause Construction is a stalling strategy that enhances a theorem prover's performance by reducing the work to construct clauses to a minimum. Instead of constructing every conclusion (clause) of an applied inference rule, the information to construct such clause is temporarily stored until the theorem prover decides to either discard the clause or construct it. If the theorem prover decides to keep the clause, it will be constructed and stored in memory, otherwise the information to construct the clause is erased. Storing the information from which an inferred clause can be constructed require almost no additional CPU operations. However, constructing a clause may consume a lot of time. Some theorem provers spend 30%–40% of their total execution time constructing and deleting clauses. With DCC this wasted time can be salvaged. DCC is useful when too many intermediate clauses (especially first order clauses) are being constructed and discarded in a short period of time because the operations performed to construct such short lived clauses are avoided. DCC may not be very effective on theorems with only propositional clauses.
ДКК қалай жұмыс істейді?
Түсіндіру ережесі қолданылған сайын, кейбір айнымалыларды терминдермен алмастыру қажет болуы мүмкін (мысалы, x → f(a)) және осылайша алмастыру жиыны қалыптасады. Нәтижедегі клаузаны құрастырып, алмастыру жиынын жоюдың орнына, теореманы дәлелдеуші жай ғана алмастыру жиынын, сондай-ақ басқа да ақпаратты сақтайды, мысалы, қандай клаузалар түсіндіру ережесіне қатысқан және қандай түсіндіру ережесі қолданылған. Содан кейін теореманы дәлелдеуші түсіндіру ережесінің нәтижесіндегі клаузаны құрастырмай, дәлелдеуді жалғастыра береді. Бұл процедура теореманы дәлелдеуші белгілі бір критерийлер мен эвристикалар негізінде, дәлелдеудің соңғы клаузасын (және, мүмкін, жол бойындағы басқа да клаузаларды) құрастыруға немесе бүкіл дәлелдеуді жоюға, яғни сақталған алмастыру жиындарын және олармен бірге сақталған барлық ақпаратты жадтан өшіруге шешім қабылдағанға дейін жалғасады.
After every application of an inference rule, certain variables may have to be substituted by terms (e. g. x → f(a)) and thus a substitution set is formed. Instead of constructing the resulting clause and discarding the substitution set, the theorem prover simply maintains the substitution set along with some other information, like what clauses where involved in the inference rule and what inference rule was applied, and continues the derivation without constructing the resulting clause of the inference rule. This procedure keeps going along a derivation until the theorem provers reaches a point where it decides, based on certain criteria and heuristics, whether to construct the final clause in the derivation (and probably some other clause(s) along the path) or discard the whole derivation i. e., deletes from memory the maintained substitution sets and whatever information stored with them.