Кіріспе
Аксиомалардан логикалық қорытынды шығару арқылы теореманы дәлелдеу. Логика мен математикада формальді дәлелдеме немесе туынды – бұл сөйлемдердің (формальді тілде жақсы құрылған формулалар) шекті тізбегі, олардың әрқайсысы аксиома, болжам немесе тізбектегі алдыңғы сөйлемдерден қорытынды шығару ережесі арқылы туындайды. Бұл табиғи тілдегі аргументтен қатаңдығы, нақтылығы және механикалық тексерілу мүмкіндігімен ерекшеленеді. Егер болжамдар жиыны бос болса, онда формальді дәлелдеменің соңғы сөйлемі формальді жүйенің теоремасы деп аталады. Теорема ұғымы әдетте тиімді емес, сондықтан берілген сөйлемнің дәлелін табуға немесе оның жоқтығын анықтауға әрқашан мүмкіндік бола бермейді. Фич стиліндегі дәлелдеме, реттік есептеу және табиғи дедукция ұғымдары – дәлелдеме ұғымының жалпылама түрі болып табылады. Теорема – дәлелдемеде оған дейінгі барлық жақсы құрылған формулалардың синтаксистік салдары. Жақсы құрылған формуланың дәлелдеменің бөлігі ретінде қарастырылуы үшін, ол дәлелдеме тізбегіндегі алдыңғы жақсы құрылған формулаларға дедуктивті аппараттың (кейбір формальді жүйенің) ережесін қолдану нәтижесі болуы керек. Формальді дәлелдемелер көбінесе интерактивті теореманы дәлелдеу кезінде компьютерлердің көмегімен құрастырылады (мысалы, дәлелдеуші және автоматтандырылған теореманы дәлелдеуші арқылы). Мұндай дәлелдемелерді автоматты түрде, соның ішінде компьютер арқылы тексеруге болады. Формальді дәлелдемелерді тексеру әдетте оңай, ал дәлелдемелерді табу мәселесі (автоматтандырылған теореманы дәлелдеу) көбінесе есептеу жағынан қиын және/немесе тек жартылай шешіледі, қолданылатын формальді жүйеге байланысты.
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference. It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable. If the set of assumptions is empty, then the last sentence in a formal proof is called a theorem of the formal system. The notion of theorem is not in general effective, therefore there may be no method by which we can always find a proof of a given sentence or determine that none exists. The concepts of Fitch style proof, sequent calculus and natural deduction are generalizations of the concept of proof. The theorem is a syntactic consequence of all the well formed formulas preceding it in the proof. For a well formed formula to qualify as part of a proof, it must be the result of applying a rule of the deductive apparatus (of some formal system) to the previous well formed formulas in the proof sequence. Formal proofs often are constructed with the help of computers in interactive theorem proving (e. g., through the use of proof checker and automated theorem prover). Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, while the problem of finding proofs (automated theorem proving) is usually computationally intractable and/or only semi decidable, depending upon the formal system in use.
Ресми тіл
Ресми тіл – символдардың шекті тізбектерінің жиынтығы. Мұндай тіл өзінің кез келген өрнегінің мағынасына сілтеме жасамай анықталуы мүмкін; ол кез келген түсіндірме берілгенге дейін, яғни мағынаға ие болмас бұрын да болуы мүмкін. Ресми дәлелдемелер кейбір ресми тілдерде жазылады.
Ресми грамматика
Формалды грамматика (оны формалау ережелері деп те атайды) – формалды тілдің дұрыс құрылған формулаларының нақты сипаттамасы. Ол формалды тіл әліпбиінің әріптерінен құралған, дұрыс құрылған формулалардың барлық тізбектерімен теңдес. Дегенмен, ол олардың семантикасын (яғни, олардың мағынасын) сипаттамайды.
Ресми жүйелер
Формалды жүйе (логикалық есептеу немесе логикалық жүйе деп те аталады) формалды тіл мен дедуктивті аппараттан (дедуктивті жүйе деп те аталады) тұрады. Дедуктивті аппарат трансформация ережелерінің (тұжырым ережелері деп те аталады) жиынтығынан, аксиомалар жиынтығынан немесе олардың екеуінен де құралуы мүмкін. Формалды жүйе басқа бір немесе бірнеше өрнектерден жаңа өрнек шығару үшін қолданылады.
Түсіндірме
Ресми жүйені түсіндіру – жүйенің символдарына мағына және оның сөйлемдеріне шындық мәнін тағайындау. Түсіндірілімдерді зерттеу формальды семантика деп аталады. Түсіндіру беру модель құрумен тең.