@prefix rdf: . @prefix dbpedia: . @prefix opencyc: . dbpedia:Proof_theory rdf:type opencyc:Mx4rvVi3_JwpEbGdrcN5Y29ycA . @prefix owl: . dbpedia:Proof_theory owl:sameAs , opencyc:Mx4rvWRWVpwpEbGdrcN5Y29ycA . @prefix ns4: . dbpedia:Proof_theory owl:sameAs ns4:Mx4rvWRWVpwpEbGdrcN5Y29ycA . @prefix foaf: . @prefix ns6: . dbpedia:Proof_theory foaf:page ns6:Proof_theory . @prefix dbpprop: . dbpedia:Proof_theory dbpprop:reference , , . @prefix rdfs: . dbpedia:Proof_theory rdfs:label "\u8BC1\u660E\u8BBA"@zh , "\u8A3C\u660E\u8AD6"@ja , "Teoria dowodu"@pl , "\u0422\u0435\u043E\u0440\u0438\u044F \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432"@ru , "Th\u00E9orie de la d\u00E9monstration"@fr , "Teor\u00EDa de la demostraci\u00F3n"@es , "Proof theory"@en , "Beweistheorie"@de , "Bewijstheorie"@nl ; dbpprop:abstract "Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt. Dies erm\u00F6glicht ihre Analyse mit mathematischen Techniken. Beweise werden \u00FCblicherweise als induktiv definierte Datenstrukturen dargestellt, wie Listen oder B\u00E4ume. Diese werden gem\u00E4\u00DF den Axiomen und Schlussregeln des betrachteten logischen Systems konstruiert. Die Beweistheorie ist von syntaktischer Natur im Gegensatz zur Modelltheorie, die von semantischer Natur ist. Manchmal wird die Beweistheorie auch als Teil der philosophischen Logik aufgefasst, dabei ist vor allem die Idee der beweistheoretischen Semantik von Interesse."@de , "La th\u00E9orie de la d\u00E9monstration, aussi connue sous le nom de th\u00E9orie de la preuve (de l'anglais proof theory), est une branche de la logique math\u00E9matique. Elle a \u00E9t\u00E9 fond\u00E9e par David Hilbert au d\u00E9but du XX si\u00E8cle. Hilbert a propos\u00E9 cette nouvelle discipline math\u00E9matique lors de son c\u00E9l\u00E8bre expos\u00E9 au 2 Congr\u00E8s international de math\u00E9matiques en 1900 avec pour objectif de r\u00E9soudre le probl\u00E8me de la coh\u00E9rence des math\u00E9matiques. Cet objectif a \u00E9t\u00E9 invalid\u00E9 par le non moins c\u00E9l\u00E8bre th\u00E9or\u00E8me d'incompl\u00E9tude de G\u00F6del en 1931, ce qui n'a toutefois pas emp\u00EAch\u00E9 la th\u00E9orie de la d\u00E9monstration de se d\u00E9velopper, notamment gr\u00E2ce aux travaux de Jacques Herbrand et de Gerhard Gentzen. Ce dernier a d\u00E9montr\u00E9 l'un des r\u00E9sultats principaux de la th\u00E9orie de la d\u00E9monstration, connu sous le nom de Hauptsatz (th\u00E9or\u00E8me principal) ou th\u00E9or\u00E8me d'\u00E9limination des coupures. Gentzen a ensuite utilis\u00E9 ce th\u00E9or\u00E8me pour donner la premi\u00E8re preuve purement syntaxique de la coh\u00E9rence de l'arithm\u00E9tique. Apr\u00E8s une p\u00E9riode de calme, qui a tout de m\u00EAme permis d'\u00E9tablir un certain nombre d'autres r\u00E9sultats de coh\u00E9rence relative et d'esquisser une classification des th\u00E9ories axiomatiques, la th\u00E9orie de la d\u00E9monstration a connu une renaissance spectaculaire au cours des ann\u00E9es 1960 avec la d\u00E9couverte de la correspondance de Curry-Howard qui a exhib\u00E9 un lien structurel nouveau et profond entre logique et informatique : essentiellement la proc\u00E9dure d'\u00E9limination des coupures d\u00E9finie par Gentzen peut \u00EAtre vue comme un processus de calcul, si bien que les d\u00E9monstrations formelles deviennent alors des programmes dont le type est la proposition \u00E0 d\u00E9montrer. Depuis, la th\u00E9orie de la d\u00E9monstration s'est d\u00E9velopp\u00E9e en \u00E9troite symbiose avec d'autres domaines de la logique et de l'informatique th\u00E9orique, notamment le lambda-calcul, et a donn\u00E9 naissance \u00E0 de nouveaux mod\u00E8les du calcul, le plus r\u00E9cent \u00E9tant la logique lin\u00E9aire de Jean-Yves Girard en 1986. Aujourd'hui, une partie de la th\u00E9orie de la d\u00E9monstration se confond avec la s\u00E9mantique des langages de programmation et interagit avec de nombreuses autres disciplines de la logique ou de l'informatique th\u00E9orique : calcul des pr\u00E9dicats calcul des propositions calcul des s\u00E9quents d\u00E9duction naturelle syst\u00E8me \u00E0 la Hilbert lambda-calcul logique combinatoire logique lin\u00E9aire Automate cellulaire programmation fonctionnelle r\u00E9alisabilit\u00E9 Th\u00E9orie des cat\u00E9gories s\u00E9mantique d\u00E9notationnelle Th\u00E9orie des jeux th\u00E9or\u00E8me de Herbrand th\u00E9orie des domaines th\u00E9orie des types linguistique"@fr , "\u0422\u0435\u043E\u0440\u0438\u044F \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u00A0\u2014 \u0440\u0430\u0437\u0434\u0435\u043B \u043C\u0430\u0442\u0435\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0439 \u043B\u043E\u0433\u0438\u043A\u0438, \u0432 \u043A\u043E\u0442\u043E\u0440\u043E\u043C \u0444\u0435\u043D\u043E\u043C\u0435\u043D \u043C\u0430\u0442\u0435\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0433\u043E \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u0430 \u0441\u0430\u043C \u0441\u0442\u0430\u043D\u043E\u0432\u0438\u0442\u0441\u044F \u043E\u0431\u044A\u0435\u043A\u0442\u043E\u043C, \u043D\u0430\u043F\u0440\u0438\u043C\u0435\u0440 \u0430\u043B\u0433\u0435\u0431\u0440\u044B \u0438\u043B\u0438 \u0430\u0440\u0438\u0444\u043C\u0435\u0442\u0438\u043A\u0438. \u0414\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u043E \u043E\u0431\u044B\u0447\u043D\u043E \u043F\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043B\u044F\u044E\u0442 \u043A\u0430\u043A \u0438\u043D\u0434\u0443\u043A\u0442\u0438\u0432\u043D\u043E \u0432\u043E\u0437\u043D\u0438\u043A\u0430\u044E\u0449\u0438\u0435 \u0441\u0442\u0440\u0443\u043A\u0442\u0443\u0440\u044B \u0434\u0430\u043D\u043D\u044B\u0445, \u043D\u0430\u0447\u0438\u043D\u0430\u044F \u0441 \u043F\u0440\u043E\u0441\u0442\u0435\u0439\u0448\u0438\u0445, \u0442\u0430\u043A\u0438\u0445 \u043A\u0430\u043A \u043F\u043B\u043E\u0441\u043A\u0438\u0435 \u0441\u043F\u0438\u0441\u043A\u0438, \u0434\u0435\u0440\u0435\u0432\u044C\u044F, \u0432\u043F\u043B\u043E\u0442\u044C \u0434\u043E \u0433\u0438\u043F\u043E\u0442\u0435\u0442\u0438\u0447\u0435\u0441\u043A\u0438\u0445 \u043F\u0440\u0435\u0434\u0435\u043B\u044C\u043D\u043E \u0441\u043B\u043E\u0436\u043D\u044B\u0445 \u0441\u0442\u0440\u0443\u043A\u0442\u0443\u0440/\u043C\u0430\u0448\u0438\u043D \u043A\u043E\u0442\u043E\u0440\u044B\u0435 \u0441\u0442\u0440\u043E\u044F\u0442\u0441\u044F \u0432 \u0441\u043E\u043E\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0438 \u0441 \u0430\u043A\u0441\u0438\u043E\u043C\u0430\u043C\u0438 \u0438 \u043F\u0440\u0430\u0432\u0438\u043B\u0430\u043C\u0438 \u0432\u044B\u0432\u043E\u0434\u0430 \u043B\u043E\u0433\u0438\u0447\u0435\u0441\u043A\u0438\u0445 \u0441\u0438\u0441\u0442\u0435\u043C, \u0438\u043C\u0435\u044E\u0449\u0438\u0445 \u0441\u043E\u043E\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044E\u0449\u0438\u0435 \u0441\u043B\u043E\u0436\u043D\u043E\u0441\u0442\u0438/\u0445\u043E\u043B\u0438\u0441\u0442\u0438\u0447\u043D\u043E\u0441\u0442\u0438 \u0441\u0435\u043C\u0430\u043D\u0442\u0438\u043A. \u0415\u0441\u043B\u0438 \u0441\u0438\u043D\u0442\u0430\u043A\u0441\u0438\u0441 \u0438 \u0441\u0435\u043C\u0430\u043D\u0442\u0438\u043A\u0443 \u043B\u043E\u0433\u0438\u043A\u0438 \u043F\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u0442\u044C \u043A\u0430\u043A \u0434\u0432\u0435 \u043F\u043E\u043B\u044F\u0440\u043D\u044B\u0435 \u0442\u043E\u0447\u043A\u0438, \u0442\u043E \u0442\u0435\u043E\u0440\u0438\u044F \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432 \u043B\u0435\u0436\u0438\u0442 \u0432 \u043E\u0431\u043B\u0430\u0441\u0442\u0438 \u0441\u0438\u043D\u0442\u0430\u043A\u0441\u0438\u0441\u0430, \u0430 \u043C\u043E\u0434\u0435\u043B\u044C\u043D\u0430\u044F \u0442\u0435\u043E\u0440\u0438\u044F \u0432 \u043E\u0431\u043B\u0430\u0441\u0442\u0438 \u0441\u0435\u043C\u0430\u043D\u0442\u0438\u043A\u0438. \u0414\u0440\u0443\u0433\u0438\u043C\u0438 \u043F\u043E\u043B\u044E\u0441\u0430\u043C\u0438 \u043B\u043E\u0433\u0438\u043A\u0438 \u043C\u043E\u0433\u0443\u0442 \u0431\u044B\u0442\u044C \u0432\u0435\u0440\u043E\u044F\u0442\u043D\u043E\u0441\u0442\u044C, \u0432\u043E\u0437\u043C\u043E\u0436\u043D\u043E\u0441\u0442\u044C \u0438\u00A0\u0442. \u00A0\u0434. \u041A\u043E\u043C\u043F\u044C\u044E\u0442\u0435\u0440\u044B \u044F\u0432\u043B\u044F\u044E\u0442\u0441\u044F \u0441\u0440\u0435\u0437\u043E\u043C \u0441\u0438\u043D\u0442\u0430\u043A\u0441\u0438\u0441\u0430/\u0441\u0435\u043C\u0430\u043D\u0442\u0438\u043A\u0438 \u043B\u043E\u0433\u0438\u043A\u0438. \u0412 \u043B\u043E\u0433\u0438\u043A\u0435 \u043A\u043E\u043C\u043F\u044C\u044E\u0442\u0435\u0440\u044B \u0432\u043E\u0441\u043F\u0440\u0438\u043D\u0438\u043C\u0430\u044E\u0442\u0441\u044F \u043F\u043B\u0430\u0442\u043E\u043D\u0438\u0447\u0435\u0441\u043A\u0438, \u043A\u0430\u043A \u043D\u0435\u043A\u0438\u0439 \u0430\u0431\u0441\u043E\u043B\u044E\u0442, \u0432 \u043A\u043E\u0442\u043E\u0440\u043E\u043C \u043C\u0430\u0448\u0438\u043D\u0430 \u0422\u044C\u044E\u0440\u0438\u043D\u0433\u0430\u00A0\u2014 \u043E\u0434\u043D\u0430 \u0438\u0437 \u0442\u043E\u0447\u0435\u043A \u043E\u0441\u043D\u043E\u0432\u0430\u043D\u0438\u044F \u043F\u0438\u0440\u0430\u043C\u0438\u0434\u044B, \u043D\u0430\u0440\u044F\u0434\u0443 \u0441 \u0436\u0438\u0432\u043E\u0439 \u043A\u043B\u0435\u0442\u043A\u043E\u0439, \u0430 \u0432\u0435\u0440\u0448\u0438\u043D\u0430\u00A0\u2014 \u043A\u0430\u043A \u043D\u0435\u043A\u0438\u0439 \u0410\u0431\u0441\u043E\u043B\u044E\u0442\u043D\u044B\u0439 \u0414\u0443\u0445 \u0432 \u0441\u0442\u0438\u043B\u0435 \u0413\u0435\u0433\u0435\u043B\u044F. \u0422\u043E \u0435\u0441\u0442\u044C \u043F\u0440\u0438\u043D\u0446\u0438\u043F\u0438\u0430\u043B\u044C\u043D\u043E \u0440\u0430\u0437\u043B\u0438\u0447\u043D\u044B\u0445 \u0442\u0438\u043F\u043E\u0432 \u043C\u0430\u0448\u0438\u043D \u0438 \u043E\u0440\u0433\u0430\u043D\u0438\u0437\u043C\u043E\u0432 \u0431\u0435\u0441\u043A\u043E\u043D\u0435\u0447\u043D\u043E \u043C\u043D\u043E\u0433\u043E. \u041E\u0434\u043D\u043E\u0439 \u0438\u0437 \u043C\u043E\u0434\u0435\u043B\u0435\u0439, \u0446\u0435\u043B\u044C\u044E \u043A\u043E\u0442\u043E\u0440\u044B\u0445 \u0431\u044B\u043B \u043C\u0430\u0442\u0435\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u0438\u0445 \u0443\u043D\u0438\u0432\u0435\u0440\u0441\u0443\u043C \u0431\u044B\u043B\u0438 \u0440\u0430\u0431\u043E\u0442\u044B \u0413\u043E\u0442\u043B\u043E\u0431\u0430 \u0424\u0440\u0435\u0433\u0435 \u0438\u043B\u0438 \u043F\u0430\u0440\u0430\u043B\u043B\u0435\u043B\u044C\u043D\u0430\u044F \u043A\u043E\u043D\u0446\u0435\u043F\u0446\u0438\u044F \u0442\u0430\u043A \u043D\u0430\u0437\u044B\u0432\u0430\u0435\u043C\u044B\u0445 \u00AB\u043E\u0441\u043D\u043E\u0432\u0430\u043D\u0438\u0439 \u043C\u0430\u0442\u0435\u043C\u0430\u0442\u0438\u043A\u0438\u00BB \u0413\u0438\u043B\u044C\u0431\u0435\u0440\u0442\u0430. \u0412 \u043D\u0435\u0451 \u043D\u0430\u0440\u044F\u0434\u0443 \u0441 \u0442\u0435\u043E\u0440\u0438\u0435\u0439 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432 \u0432\u0445\u043E\u0434\u0438\u043B\u0438 \u0442\u0430\u043A\u0436\u0435 \u0442\u0435\u043E\u0440\u0438\u044F \u043C\u043E\u0434\u0435\u043B\u0435\u0439, \u0430\u043A\u0441\u0438\u043E\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u0430\u044F \u0442\u0435\u043E\u0440\u0438\u044F \u043C\u043D\u043E\u0436\u0435\u0441\u0442\u0432, \u0442\u0435\u043E\u0440\u0438\u0435\u0439 \u0440\u0435\u043A\u0443\u0440\u0441\u0438\u0438. \u0422\u0435\u043E\u0440\u0438\u044F \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u0430 \u043C\u043E\u0436\u0435\u0442 \u0440\u0430\u0441\u0441\u043C\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044C\u0441\u044F \u043A\u0430\u043A \u0432\u0435\u0442\u0432\u044C \u0444\u0438\u043B\u043E\u0441\u043E\u0444\u0441\u043A\u043E\u0439 \u043B\u043E\u0433\u0438\u043A\u0438, \u0432 \u043A\u043E\u0442\u043E\u0440\u043E\u0439 \u043E\u0441\u043D\u043E\u0432\u043D\u043E\u0439 \u0438\u043D\u0442\u0435\u0440\u0435\u0441 \u043F\u0440\u043E\u0435\u043A\u0442\u0438\u0432\u043D\u044B\u0439 \u043F\u043E\u0442\u0435\u043D\u0446\u0438\u0430\u043B \u0438\u043B\u0438 \u0441\u0435\u043C\u0430\u043D\u0442\u0438\u043A\u0430 \u0442\u0435\u043E\u0440\u0438\u0438 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432 (proof-theoretic semantics), \u0438 \u043E\u0431\u0440\u0430\u0442\u043D\u0430\u044F \u0437\u0430\u0434\u0430\u0447\u0430 \u043D\u0430\u0445\u043E\u0436\u0434\u0435\u043D\u0438\u044F/\u043A\u043E\u043D\u0441\u0442\u0440\u0443\u0438\u0440\u043E\u0432\u0430\u043D\u0438\u044F \u043C\u0430\u0448\u0438\u043D \u0438 \u043F\u0443\u0442\u0438 \u0432 \u043B\u043E\u0433\u0438\u0447\u0435\u0441\u043A\u043E\u043C \u0443\u043D\u0438\u0432\u0435\u0440\u0441\u0443\u043C\u0435 \u043C\u0435\u0436\u0443 \u0438\u0441\u0445\u043E\u0434\u043D\u044B\u043C\u0438 \u0434\u0430\u043D\u043D\u044B\u043C\u0438 \u0438 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u043E\u043C."@ru , "Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature. Together with model theory, axiomatic set theory, and recursion theory, proof theory is one of the so-called four pillars of the foundations of mathematics. Proof theory is important in philosophical logic, where the primary interest is in the idea of a proof-theoretic semantics, an idea which depends upon technical ideas in structural proof theory to be feasible."@en , "\u8A3C\u660E\u8AD6\uFF08\u82F1: Proof theory\uFF09\u306F\u3001\u6570\u7406\u8AD6\u7406\u5B66\u306E\u4E00\u5206\u91CE\u3067\u3042\u308A\u3001\u8A3C\u660E\u3092\u6570\u5B66\u7684\u30AA\u30D6\u30B8\u30A7\u30AF\u30C8\u3068\u3057\u3066\u5F62\u5F0F\u7684\u306B\u8868\u3057\u3001\u305D\u308C\u306B\u6570\u5B66\u7684\u89E3\u6790\u3092\u65BD\u3059\u3002\u8A3C\u660E\u306F\u5E30\u7D0D\u7684\u306B\u5B9A\u7FA9\u3055\u308C\u305F\u30C7\u30FC\u30BF\u69CB\u9020\u3067\u8868\u3055\u308C\u308B\u3053\u3068\u304C\u591A\u304F\u3001\u5358\u7D14\u306A\u30EA\u30B9\u30C8\u3001\u5165\u308C\u5B50\u30EA\u30B9\u30C8\u3001\u6728\u69CB\u9020\u306A\u3069\u304C\u3042\u308B\u3002\u3053\u308C\u3089\u306F\u8AD6\u7406\u4F53\u7CFB\u306E\u516C\u7406\u3084\u63A8\u8AD6\u898F\u5247\u306B\u3088\u3063\u3066\u69CB\u7BC9\u3055\u308C\u308B\u3002\u305D\u306E\u305F\u3081\u3001\u8A3C\u660E\u8AD6\u306B\u306F\u7D71\u8F9E\u8AD6\u7684\u6027\u8CEA\u304C\u3042\u308B\u304C\u3001\u5BFE\u7167\u7684\u306B\u30E2\u30C7\u30EB\u7406\u8AD6\u306B\u306F\u610F\u5473\u8AD6\u7684\u6027\u8CEA\u304C\u3042\u308B\u3002\u30E2\u30C7\u30EB\u7406\u8AD6\u3001\u516C\u7406\u7684\u96C6\u5408\u8AD6\u3001\u518D\u5E30\u7406\u8AD6\u306A\u3069\u3068\u5171\u306B\u6570\u5B66\u57FA\u790E\u8AD6\u306E\u56DB\u672C\u67F1\u3068\u3055\u308C\u3066\u3044\u308B\u3002\u8A3C\u660E\u8AD6\u306F\u54F2\u5B66\u7684\u8AD6\u7406\u5B66\u306E\u4E00\u5206\u91CE\u3068\u898B\u308B\u3053\u3068\u3082\u3067\u304D\u3001\u305D\u306E\u5834\u5408\u306E\u4E3B\u8981\u306A\u8208\u5473\u306F\u8A3C\u660E\u8AD6\u7684\u610F\u5473\u8AD6\u3067\u3042\u308A\u3001\u305D\u306E\u6280\u6CD5\u7684\u57FA\u790E\u3068\u3057\u3066\u69CB\u9020\u8A3C\u660E\u8AD6\uFF08structural proof theory\uFF09\u306E\u8003\u3048\u65B9\u304C\u3042\u308B\u3002"@ja , "Teoria dowodu to dzia\u0142 logiki matematycznej zajmuj\u0105cy si\u0119 analiz\u0105 poj\u0119cia dowodu oraz mo\u017Cliwych sposob\u00F3w u\u017Cywania go w rozwa\u017Caniach matematycznych. Za ojca tej dziedziny uwa\u017Ca si\u0119 Davida Hilberta, jednego z najwybitniejszych matematyk\u00F3w prze\u0142omu dziewi\u0119tnastego i dwudziestego wieku. Do g\u0142\u00F3wnych zada\u0144 teorii dowodu nale\u017Cy kszta\u0142towanie takich system\u00F3w logicznych wraz z odpowiednimi zestawami aksjomat\u00F3w, kt\u00F3re nadawa\u0142yby si\u0119 do formalizowania dowod\u00F3w matematycznych, nast\u0119pnie za\u015B badanie si\u0142y tych system\u00F3w (im silniejszy system, tym wi\u0119cej twierdze\u0144 mo\u017Cna udowodni\u0107 na jego gruncie wychodz\u0105c z danego zbioru aksjomat\u00F3w). Bada si\u0119 te\u017C szczeg\u00F3\u0142owo struktur\u0119 dowod\u00F3w formalnych, co czyni teori\u0119 dowodu odpowiednikiem syntaktyki logicznej (czasem obu tych termin\u00F3w u\u017Cywa si\u0119 zamiennie)."@pl , "La teor\u00EDa de la demostraci\u00F3n o teor\u00EDa de la prueba es una rama de la l\u00F3gica matem\u00E1tica que trata a las demostraciones como objetos matem\u00E1ticos, facilitando su an\u00E1lisis mediante t\u00E9cnicas matem\u00E1ticas. Las demostraciones suelen presentarse como estructuras de datos inductivamente definidas que se construyen de acuerdo con los axiomas y reglas de inferencia de los sistemas l\u00F3gicos. En este sentido, la teor\u00EDa de la demostraci\u00F3n se ocupa de la sintaxis, en contraste con la teor\u00EDa de modelos, que trata con la sem\u00E1ntica. Junto con la teor\u00EDa de modelos, la teor\u00EDa de conjuntos axiom\u00E1tica y la teor\u00EDa de la recursi\u00F3n, la teor\u00EDa de la demostraci\u00F3n es uno de los \"cuatro pilares\" de los fundamentos de las matem\u00E1ticas."@es , "Bewijstheorie is een tak van de wiskundige logica die bewijzen als formele wiskundig objecten opvat. Hierdoor kunnen bewijzen door middel van wiskundige technieken worden geanalyseerd. Bewijzen worden meestal gepresenteerd als inductief gedefinieerde datastructuren, zoals gewone lijsten, boxed lijsten, of boomstructuren, die volgens de axioma's en afleidingsregels van het logisch systeem worden geconstrueerd. Als zodanig is de bewijstheorie syntactisch van aard, dit in tegenstelling tot de modeltheorie, die van nature semantisch is. Samen met de modeltheorie, de axiomatische verzamelingenleer en de recursietheorie wordt de bewijstheorie gezien als \u00E9\u00E9n van de vier zogenaamde pilaren van de grondslagen van de wiskunde. Bewijs theorie kan ook beschouwd worden als een tak van de filosofische logica, waar het primaire interessegebied in het idee van een bewijs-theoretische semantiek ligt, een opvatting die afhangt van het feit of bepaalde technische idee\u00EBn in de structurele bewijstheorie al of niet haalbaar zijn."@nl , "\u8BC1\u660E\u8BBA\u662F\u6570\u7406\u903B\u8F91\u7684\u4E00\u4E2A\u5206\u652F\uFF0C\u5B83\u5C06\u6570\u5B66\u8BC1\u660E\u8868\u8FBE\u4E3A\u5F62\u5F0F\u5316\u7684\u6570\u5B66\u5BA2\u4F53\uFF0C\u4ECE\u800C\u901A\u8FC7\u6570\u5B66\u6280\u672F\u6765\u7B80\u5316\u5BF9\u4ED6\u4EEC\u7684\u5206\u6790\u3002\u8BC1\u660E\u901A\u5E38\u7528\u5F52\u7EB3\u5F0F\u5730\u5B9A\u4E49\u7684\u6570\u636E\u7ED3\u6784\u6765\u8868\u8FBE\uFF0C\u4F8B\u5982\u94FE\u8868\uFF0C\u76D2\u94FE\u8868\uFF0C\u6216\u8005\u6811\uFF0C\u5B83\u4EEC\u6839\u636E\u903B\u8F91\u7CFB\u7EDF\u7684\u516C\u7406\u548C\u63A8\u7406\u89C4\u5219\u6784\u9020\u3002\u56E0\u6B64\uFF0C\u8BC1\u660E\u8BBA\u672C\u8D28\u4E0A\u662F\u8BED\u6CD5\u903B\u8F91\uFF0C\u548C\u672C\u8D28\u4E0A\u662F\u8BED\u4E49\u5B66\u7684\u6A21\u578B\u8BBA\u5F62\u76F8\u53CD\u3002\u548C\u6A21\u578B\u8BBA\uFF0C\u516C\u7406\u5316\u96C6\u5408\u8BBA\uFF0C\u4EE5\u53CA\u9012\u5F52\u8BBA\u4E00\u8D77\uFF0C\u8BC1\u660E\u8BBA\u88AB\u79F0\u4E3A\u6570\u5B66\u57FA\u7840\u7684\u56DB\u5927\u652F\u67F1\u4E4B\u4E00\u3002 \u8BC1\u660E\u8BBA\u4E5F\u53EF\u89C6\u4E3A\u54F2\u5B66\u903B\u8F91\u7684\u5206\u652F\uFF0C\u5176\u4E3B\u8981\u5174\u8DA3\u5728\u4E8E\u8BC1\u660E\u8BBA\u8BED\u4E49\u5B66\u7684\u601D\u60F3\uFF0C\u8BE5\u601D\u60F3\u4F9D\u8D56\u4E8E\u7ED3\u6784\u8BC1\u660E\u8BBA\u7684\u6280\u672F\u578B\u60F3\u6CD5\u624D\u53EF\u884C\u3002"@zh ; rdfs:comment "Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt. Dies erm\u00F6glicht ihre Analyse mit mathematischen Techniken. Beweise werden \u00FCblicherweise als induktiv definierte Datenstrukturen dargestellt, wie Listen oder B\u00E4ume. Diese werden gem\u00E4\u00DF den Axiomen und Schlussregeln des betrachteten logischen Systems konstruiert. Die Beweistheorie ist von syntaktischer Natur im Gegensatz zur Modelltheorie, die von semantischer Natur ist."@de , ""@zh , "Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature."@en , ""@ja , "Teoria dowodu to dzia\u0142 logiki matematycznej zajmuj\u0105cy si\u0119 analiz\u0105 poj\u0119cia dowodu oraz mo\u017Cliwych sposob\u00F3w u\u017Cywania go w rozwa\u017Caniach matematycznych. Za ojca tej dziedziny uwa\u017Ca si\u0119 Davida Hilberta, jednego z najwybitniejszych matematyk\u00F3w prze\u0142omu dziewi\u0119tnastego i dwudziestego wieku."@pl , "La th\u00E9orie de la d\u00E9monstration, aussi connue sous le nom de th\u00E9orie de la preuve (de l'anglais proof theory), est une branche de la logique math\u00E9matique. Elle a \u00E9t\u00E9 fond\u00E9e par David Hilbert au d\u00E9but du XX si\u00E8cle. Hilbert a propos\u00E9 cette nouvelle discipline math\u00E9matique lors de son c\u00E9l\u00E8bre expos\u00E9 au 2 Congr\u00E8s international de math\u00E9matiques en 1900 avec pour objectif de r\u00E9soudre le probl\u00E8me de la coh\u00E9rence des math\u00E9matiques."@fr , "La teor\u00EDa de la demostraci\u00F3n o teor\u00EDa de la prueba es una rama de la l\u00F3gica matem\u00E1tica que trata a las demostraciones como objetos matem\u00E1ticos, facilitando su an\u00E1lisis mediante t\u00E9cnicas matem\u00E1ticas. Las demostraciones suelen presentarse como estructuras de datos inductivamente definidas que se construyen de acuerdo con los axiomas y reglas de inferencia de los sistemas l\u00F3gicos."@es , "Bewijstheorie is een tak van de wiskundige logica die bewijzen als formele wiskundig objecten opvat. Hierdoor kunnen bewijzen door middel van wiskundige technieken worden geanalyseerd. Bewijzen worden meestal gepresenteerd als inductief gedefinieerde datastructuren, zoals gewone lijsten, boxed lijsten, of boomstructuren, die volgens de axioma's en afleidingsregels van het logisch systeem worden geconstrueerd."@nl , "\u0422\u0435\u043E\u0440\u0438\u044F \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u00A0\u2014 \u0440\u0430\u0437\u0434\u0435\u043B \u043C\u0430\u0442\u0435\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0439 \u043B\u043E\u0433\u0438\u043A\u0438, \u0432 \u043A\u043E\u0442\u043E\u0440\u043E\u043C \u0444\u0435\u043D\u043E\u043C\u0435\u043D \u043C\u0430\u0442\u0435\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0433\u043E \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u0430 \u0441\u0430\u043C \u0441\u0442\u0430\u043D\u043E\u0432\u0438\u0442\u0441\u044F \u043E\u0431\u044A\u0435\u043A\u0442\u043E\u043C, \u043D\u0430\u043F\u0440\u0438\u043C\u0435\u0440 \u0430\u043B\u0433\u0435\u0431\u0440\u044B \u0438\u043B\u0438 \u0430\u0440\u0438\u0444\u043C\u0435\u0442\u0438\u043A\u0438."@ru . @prefix skos: . @prefix ns10: . dbpedia:Proof_theory skos:subject ns10:Proof_theory , ns10:Mathematical_logic , ns10:Logic . @prefix ns11: . dbpedia:Proof_theory dbpprop:hasPhotoCollection ns11:Proof_theory . @prefix dbpedia-owl: . dbpedia:Rohit_Jivanlal_Parikh dbpedia-owl:knownFor dbpedia:Proof_theory . @prefix ns13: . dbpedia:Rohit_Jivanlal_Parikh ns13:knownFor dbpedia:Proof_theory ; dbpprop:knownFor dbpedia:Proof_theory . dbpedia:Proof_theorist dbpprop:redirect dbpedia:Proof_theory . dbpprop:redirect dbpedia:Proof_theory . dbpedia:Proof-theoretic dbpprop:redirect dbpedia:Proof_theory .