Proof theory (original) (raw)
La teoria de la demostració és una branca de la lògica matemàtica que tracta amb l'estructura de les demostracions matemàtiques i la potència expressiva d'un determinat conjunt d'axiomes matemàtics.
| Property | Value |
|---|---|
| dbo:abstract | نظرية البرهان (بالإنجليزية: Proof theory) هي أحد فروع المنطق الرياضي الذي يتعامل مع البرهان كائنا رياضيا شكليا، مسهلا بذلك عملية تحليل البرهان بالتقنيات الرياضية. تمثل البراهين عادة بنى بيانات معرفة حدسيا، مثل القوائم المنبسطة (plain lists) أو القوائم المعلبة (boxed lists) أو الأشجار، التي تتشكل بناء على بدهيات rules of inference للنظام المنطقي. بهذا تكون نظرية البرهان بطبيعتها، بعكس نظرية النموذج أو أو نظرية الاستدعاء الذاتي. نظرية البرهان أحد ما يسمى الأعمدة الأربع . يمكن أن تعتبر نظرية البرهان أحد فروع المنطق الفلسفي أيضا، حيث يكون الاهتمام المبدئي بفكرة proof-theoretic semantics، وهي فكرة تعتمد على أفكار تقنية في structural proof theory لتكون مقبولة. (ar) La teoria de la demostració és una branca de la lògica matemàtica que tracta amb l'estructura de les demostracions matemàtiques i la potència expressiva d'un determinat conjunt d'axiomes matemàtics. (ca) Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt, was deren Analyse mit mathematischen Techniken ermöglicht. Beweise werden üblicherweise als induktiv definierte Datenstrukturen dargestellt, wie Listen oder Bäume. Diese werden gemäß 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) Pruvteorio estas grava branĉo de matematika logiko kiu reprezentas pruvojn kiel formalaj matematikaj objektoj, faciligante ties analizon pere de matematikaj teknikoj. Pruvoj estas tipe prezentita kiel indukto-difinitaj datumstrukturoj tiaj kiaj ebenlistoj, sekvaĵa kalkulo, skatoligitaj listoj, aŭ arboj, kiuj estas konstruitaj laŭ la aksiomoj kaj reguloj de inferenco de logika sistemo. Tiel, pruvteorio estas sintaksa nature, kontraste al modelteorio, kiu estas semantika nature. Kelkaj el la plej gravaj areoj de pruvteorio estas struktura pruvteorio, ordonombra analizo, provableca logiko (ne konfuzu kun probableca logiko), inversa matematiko, pruvminado, aŭtomata teorempruvado, kaj pruvkomplekseco. Multa esplorado fokusas ankaŭ al aplikaĵoj en komputa scienco, lingvistiko kaj filozofio. (eo) La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XXe siècle. Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au 2e congrès international des mathématiciens en 1900 avec pour objectif de démontrer la cohérence des mathématiques. Cet objectif a été invalidé par le non moins célèbre théorème d'incomplétude de Gödel en 1931, ce qui n'a toutefois pas empêché la théorie de la démonstration de se développer, notamment grâce aux travaux de Jacques Herbrand et de Gerhard Gentzen. Ce dernier a démontré l'un des résultats principaux de la théorie de la démonstration, connu sous le nom de Hauptsatz (théorème principal) ou théorème d'élimination des coupures. Gentzen a ensuite utilisé ce théorème pour donner la première démonstration purement syntaxique de la cohérence de l'arithmétique. Après une période de calme, qui a tout de même permis d'établir un certain nombre d'autres résultats de cohérence relative et d'esquisser une classification des théories axiomatiques, la théorie de la démonstration a connu une renaissance spectaculaire au cours des années 1960 avec la découverte de la correspondance de Curry-Howard qui a exhibé un lien structurel nouveau et profond entre logique et informatique : essentiellement, la procédure d'élimination des coupures définie par Gentzen peut être vue comme un processus de calcul, si bien que les démonstrations formelles deviennent alors des programmes dont le type est la proposition à démontrer. Depuis, la théorie de la démonstration s'est développée en étroite symbiose avec d'autres domaines de la logique et de l'informatique théorique, notamment le lambda-calcul, et a donné naissance à de nouveaux modèles du calcul, le plus récent étant la logique linéaire de Jean-Yves Girard en 1986. Aujourd'hui, une partie de la théorie de la démonstration se confond avec la sémantique des langages de programmation et interagit avec de nombreuses autres disciplines de la logique ou de l'informatique théorique : * Calcul des prédicats * Calcul des propositions * Calcul des séquents * Déduction naturelle (voir aussi Style de Fitch pour la déduction naturelle) * Système à la Hilbert * Lambda-calcul * Logique combinatoire * Logique linéaire * Automate cellulaire * Programmation fonctionnelle * Réalisabilité * Théorie des catégories * Sémantique dénotationnelle * Théorème de Herbrand * Théorie des domaines * Théorie des types * Complexité des preuves (fr) La teoría de la demostración o teoría de la prueba es una rama de la lógica matemática que trata a las demostraciones como objetos matemáticos, facilitando su análisis mediante técnicas matemáticas. 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ógicos. En este sentido, la teoría de la demostración se ocupa de la sintaxis, en contraste con la teoría de modelos, que trata con la semántica. Junto con la teoría de modelos, la teoría de conjuntos axiomática y la teoría de la computabilidad, la teoría de la demostración es uno de los «cuatro pilares» de los fundamentos de las matemáticas.[cita requerida] (es) Proof theory is a major 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 lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature. Some of the major areas of proof theory include structural proof theory, ordinal analysis, provability logic, reverse mathematics, proof mining, automated theorem proving, and proof complexity. Much research also focuses on applications in computer science, linguistics, and philosophy. (en) 証明論（しょうめいろん、英語: proof theory）は、数理論理学の一分野であり、証明を数学的対象として形式的に表し、それに数学的解析を施す。 (ja) 수리논리학에서 증명 이론(證明理論, 영어: proof theory)은 증명을 형식적인 수학적 개체로 표상하여 수학적 기법으로 이용하여 증명을 객관적으로 분석하는 이론이다. 증명은 귀납적으로 정의된 자료구조로 표현되는데, 이는 어떠한 이론체계의 공리와 추론 규칙에 따라 구성된다. 즉 모형이론에 의미론적 성질이 있는 데 대조적으로 증명 이론에는 구문론적 성질이 있다. 모형 이론, 집합론, 재귀 이론과 함께 증명 이론은 수학기초론의 4대 기둥이라고도 불린다. (ko) Bewijstheorie is een tak van de wiskundige logica die bewijzen als formele wiskundige objecten opvat. Hierdoor kunnen bewijzen door middel van wiskundige technieken worden geanalyseerd. Bewijzen worden meestal gepresenteerd als inductief gedefinieerde algoritmen, 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 een van de vier zogenaamde pilaren van de grondslagen van de wiskunde.Bewijstheorie kan ook worden beschouwd als een tak van de , waarin de bewijstheoretische semantiek het belangrijkste is. Het hangt ervan af dat bepaalde ideeën in de structurele bewijstheorie al dan niet haalbaar zijn. (nl) La teoria della dimostrazione è la branca della logica matematica che considera le dimostrazioni a loro volta come oggetti matematici, facilitando la loro analisi con tecniche matematiche. Le dimostrazioni sono solitamente presentate come strutture dati definite induttivamente (ad esempio, liste o alberi), costruite secondo gli assiomi e le regole di inferenza del sistema logico. La teoria della dimostrazione non solo gioca un ruolo primario nella teoria dei linguaggi di programmazione, ma è anche uno dei cosiddetti quattro pilastri dei fondamenti della matematica, assieme alla teoria dei modelli, alla teoria assiomatica degli insiemi e alla teoria della calcolabilità. (it) A teoria das provas, teoria da prova ou teoria da demonstração é um ramo importante da lógica matemática que representa provas como objetos matemáticos, facilitando sua análise por técnicas matemáticas. Provas são tipicamente representadas por estruturas de dados definidas indutivamente, como listas simples, listas encadeadas, árvores, cada uma construída de acordo com os axiomas e regras de inferência do sistema lógico. Consequentemente, a teoria da prova é de natureza sintática, em contraste com a teoria dos modelos que é de natureza semântica. Juntamente com a teoria dos modelos, e a teoria da computabilidade, a teoria da prova é um dos chamados quatro pilares dos fundamentos da matemática. É também importante na lógica filosófica, onde os interesses principais estão na ideia de uma semântica prova-teórica, uma ideia que, para ser viável, depende de ideias técnicas da teoria da prova estrutural. Algumas das principais áreas da teoria de prova incluem teoria da prova estrutural, , , , , prova automática de teoremas e complexidade de prova. Muitas pesquisas também se concentram em aplicações em ciência da computação, linguística e filosofia. (pt) Teoria dowodu – dział logiki matematycznej zajmujący się analizą pojęcia dowodu oraz możliwych sposobów używania go w rozważaniach matematycznych. Za ojca tej dziedziny uważa się Davida Hilberta, jednego z najwybitniejszych matematyków przełomu dziewiętnastego i dwudziestego wieku. Do głównych zadań teorii dowodu należy kształtowanie takich systemów logicznych wraz z odpowiednimi zestawami aksjomatów, które nadawałyby się do formalizowania dowodów matematycznych, następnie zaś badanie siły tych systemów (im silniejszy system, tym więcej twierdzeń można udowodnić na jego gruncie wychodząc z danego zbioru aksjomatów). Bada się też szczegółowo strukturę dowodów formalnych, co czyni teorię dowodu odpowiednikiemsyntaktyki logicznej (czasem obu tych terminów używa się zamiennie). (pl) Bevisteori är en gren av matematisk logik som representerar bevis som matematiska objekt i sig, vilket underlättar analys av dem med matematiska tekniker. Bevis beskrivs vanligtvis som induktivt definierade datastrukturer, som konstrueras enligt det logiska systemets axiom och härledningsregler. (sv) Теория доказательств — раздел математической логики, представляющий доказательства в виде формальных математических объектов, осуществляя их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определённых структур данных, таких как списки и деревья, созданных в соответствии с аксиомами и правилами вывода формальных систем. Таким образом, теория доказательств является синтаксической, в отличие от семантической теории моделей. Вместе с теорией моделей, аксиоматической теорией множеств и теорией вычислений, теория доказательств является одним из так называемых «четырёх столпов» математики. Теория доказательств использует точное определение понятия доказательства при доказательстве невозможности доказательства того или иного предложения в рамках заданной математической теории. Теория доказательств важна для философской логики, где самостоятельный интерес представляет идея теоретико-доказательственной семантики, — идея, которая основана на осуществимости формально-логических методов структурной теории доказательств. (ru) Теорія доведення (доказів) є розділом математичної логіки, який представляє докази у вигляді формальних математичних об'єктів, здійснюючи їх аналіз за допомогою математичних методів. Докази, як правило, представлені у вигляді індуктивно визначеної структури даних, таких як списки і дерева, створених відповідно до аксіом і правил виводу формальних систем. Таким чином, теорія доказів є синтаксичною, на відміну від семантичної теорії моделей. Разом з теорією моделей, аксіоматичною теорією множин та теорією обчислень, теорія доказів є одним з так званих «чотирьох стовпів» основ математики. (uk) 证明论是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。 证明论也可视为哲学逻辑的分支，其主要兴趣在于的思想，该思想依赖于的技术型想法才可行。 (zh) |
| dbo:wikiPageExternalLink | https://www.jstor.org/stable/20009142 http://plato.stanford.edu/entries/proof-theory-development/ https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/proofs-and-types.pdf https://books.google.com/books%3Fhl=en&lr=&id=MfTMDeCq7ukC&oi=fnd&pg=PP1&dq=%22Handbook+of+Proof+Theory%22&ots=LfJuyY2Fel&sig=jbYv39Cl_viSaVkHIjDF7q4e6K4%23v=onepage&q=%22Handbook%20of%20Proof%20Theory%22&f=false http://www.andrew.cmu.edu/user/avigad/Papers/infinite.pdf |
| dbo:wikiPageID | 183478 (xsd:integer) |
| dbo:wikiPageLength | 19800 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1119036403 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Predicate_logic dbr:Proof_(truth) dbr:Proof_calculi dbr:Proof_complexity dbr:Proof_net dbr:Modal_logic dbr:Model_theory dbr:Montague_grammar dbr:Löb's_theorem dbr:Typed_lambda_calculus dbr:Bertrand_Russell dbr:David_Hilbert dbr:Peano_Arithmetic dbr:Peano_arithmetic dbr:Per_Martin-Löf dbr:Reverse_mathematics dbr:Richard_Dedekind dbr:Cut-elimination_theorem dbr:Dag_Prawitz dbr:Intermediate_logic dbr:Interpretability_logic dbr:Intuitionistic_logic dbr:Intuitionistic_type_theory dbr:Elimination_rule dbr:Transfinite_induction dbr:Structural_proof_theory dbr:Analytic_proof dbc:Proof_theory dbr:Mathematical_logic dbr:Mathematical_object dbr:Gerhard_Gentzen dbr:Giuseppe_Peano dbr:Gottlob_Frege dbr:Theorem dbr:Ordinal_analysis dbr:Arithmetical_hierarchy dbr:Linear_logic dbr:Stanford_Encyclopedia_of_Philosophy dbr:Combinatorial_proof dbr:Peer_review dbr:Propositional_logic dbr:Syntax_(logic) dbr:Automated_theorem_proving dbr:Tree_(data_structure) dbr:Type_theory dbr:Harvey_Friedman dbr:Japaridze's_polymodal_logic dbr:Jon_Barwise dbr:Linguistics dbr:Alan_Turing dbr:Curry–Howard_correspondence dbr:Data_structures dbr:Formal_semantics_(logic) dbr:Diagonal_lemma dbr:Dialectica_interpretation dbr:Focused_proof dbr:Hilbert's_program dbr:Natural_deduction dbr:Mathematical_proof dbr:Relevance_logic dbr:Gödel's_incompleteness_theorems dbr:Hao_Wang_(academic) dbr:Hilbert_system dbr:J._Barkley_Rosser dbr:Jan_Łukasiewicz dbr:Jean-Yves_Girard dbc:Mathematical_logic dbr:Supremum dbr:Theory_(mathematical_logic) dbr:Zorn's_lemma dbr:Provability_logic dbr:Recursive_data_type dbr:Axiom dbr:Axiom_of_choice dbc:Metalogic dbr:Solomon_Feferman dbr:Classical_logic dbr:Grundlagen_der_Mathematik dbr:Kurt_Gödel dbr:Cartesian_closed_category dbr:Categorial_grammar dbr:Real_number dbr:Sequent_calculus dbr:Rule_of_inference dbr:Self-verifying_theories dbr:Proof_mining dbr:Stanisław_Jaśkowski dbr:Finitary dbr:Ω-consistent_theory dbr:Introduction_rule dbr:Substructural_logic dbr:Robert_Solovay dbr:List_(computer_science) dbr:Martin_Hugo_Löb dbr:Proof_techniques dbr:Van_Nostrand_(publisher) dbr:Natural_deduction_calculus dbr:Natural_language_semantics dbr:A._S._Troelstra dbr:Recursion_theory dbr:Interactive_theorem_proving dbr:Gödel's_second_incompleteness_theorem dbr:ZF_set_theory dbr:Reductive_logic dbr:Type-logical_grammar |
| dbp:b | 1 (xsd:integer) 2 (xsd:integer) |
| dbp:id | p/p075430 (en) |
| dbp:p | 1 (xsd:integer) 2 (xsd:integer) |
| dbp:title | Proof theory (en) |
| dbp:wikiPageUsesTemplate | dbt:Springer dbt:Commonscat dbt:Main dbt:Portal dbt:Short_description dbt:Vanchor dbt:Isbn dbt:Su dbt:Mathematical_logic |
| dcterms:subject | dbc:Proof_theory dbc:Mathematical_logic dbc:Metalogic |
| gold:hypernym | dbr:Branch |
| rdf:type | yago:Field108569998 yago:GeographicalArea108574314 yago:Location100027167 yago:Object100002684 yago:PhysicalEntity100001930 yago:Region108630985 yago:YagoGeoEntity yago:YagoLegalActorGeo yago:YagoPermanentlyLocatedEntity dbo:Organisation yago:Tract108673395 yago:WikicatFieldsOfMathematics |
| rdfs:comment | La teoria de la demostració és una branca de la lògica matemàtica que tracta amb l'estructura de les demostracions matemàtiques i la potència expressiva d'un determinat conjunt d'axiomes matemàtics. (ca) La teoría de la demostración o teoría de la prueba es una rama de la lógica matemática que trata a las demostraciones como objetos matemáticos, facilitando su análisis mediante técnicas matemáticas. 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ógicos. En este sentido, la teoría de la demostración se ocupa de la sintaxis, en contraste con la teoría de modelos, que trata con la semántica. Junto con la teoría de modelos, la teoría de conjuntos axiomática y la teoría de la computabilidad, la teoría de la demostración es uno de los «cuatro pilares» de los fundamentos de las matemáticas.[cita requerida] (es) 証明論（しょうめいろん、英語: proof theory）は、数理論理学の一分野であり、証明を数学的対象として形式的に表し、それに数学的解析を施す。 (ja) 수리논리학에서 증명 이론(證明理論, 영어: proof theory)은 증명을 형식적인 수학적 개체로 표상하여 수학적 기법으로 이용하여 증명을 객관적으로 분석하는 이론이다. 증명은 귀납적으로 정의된 자료구조로 표현되는데, 이는 어떠한 이론체계의 공리와 추론 규칙에 따라 구성된다. 즉 모형이론에 의미론적 성질이 있는 데 대조적으로 증명 이론에는 구문론적 성질이 있다. 모형 이론, 집합론, 재귀 이론과 함께 증명 이론은 수학기초론의 4대 기둥이라고도 불린다. (ko) Bevisteori är en gren av matematisk logik som representerar bevis som matematiska objekt i sig, vilket underlättar analys av dem med matematiska tekniker. Bevis beskrivs vanligtvis som induktivt definierade datastrukturer, som konstrueras enligt det logiska systemets axiom och härledningsregler. (sv) Теорія доведення (доказів) є розділом математичної логіки, який представляє докази у вигляді формальних математичних об'єктів, здійснюючи їх аналіз за допомогою математичних методів. Докази, як правило, представлені у вигляді індуктивно визначеної структури даних, таких як списки і дерева, створених відповідно до аксіом і правил виводу формальних систем. Таким чином, теорія доказів є синтаксичною, на відміну від семантичної теорії моделей. Разом з теорією моделей, аксіоматичною теорією множин та теорією обчислень, теорія доказів є одним з так званих «чотирьох стовпів» основ математики. (uk) 证明论是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。 证明论也可视为哲学逻辑的分支，其主要兴趣在于的思想，该思想依赖于的技术型想法才可行。 (zh) نظرية البرهان (بالإنجليزية: Proof theory) هي أحد فروع المنطق الرياضي الذي يتعامل مع البرهان كائنا رياضيا شكليا، مسهلا بذلك عملية تحليل البرهان بالتقنيات الرياضية. تمثل البراهين عادة بنى بيانات معرفة حدسيا، مثل القوائم المنبسطة (plain lists) أو القوائم المعلبة (boxed lists) أو الأشجار، التي تتشكل بناء على بدهيات rules of inference للنظام المنطقي. بهذا تكون نظرية البرهان بطبيعتها، بعكس نظرية النموذج أو أو نظرية الاستدعاء الذاتي. نظرية البرهان أحد ما يسمى الأعمدة الأربع . (ar) Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt, was deren Analyse mit mathematischen Techniken ermöglicht. Beweise werden üblicherweise als induktiv definierte Datenstrukturen dargestellt, wie Listen oder Bäume. Diese werden gemäß 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) Pruvteorio estas grava branĉo de matematika logiko kiu reprezentas pruvojn kiel formalaj matematikaj objektoj, faciligante ties analizon pere de matematikaj teknikoj. Pruvoj estas tipe prezentita kiel indukto-difinitaj datumstrukturoj tiaj kiaj ebenlistoj, sekvaĵa kalkulo, skatoligitaj listoj, aŭ arboj, kiuj estas konstruitaj laŭ la aksiomoj kaj reguloj de inferenco de logika sistemo. Tiel, pruvteorio estas sintaksa nature, kontraste al modelteorio, kiu estas semantika nature. (eo) La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XXe siècle. (fr) Proof theory is a major 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 lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature. (en) La teoria della dimostrazione è la branca della logica matematica che considera le dimostrazioni a loro volta come oggetti matematici, facilitando la loro analisi con tecniche matematiche. Le dimostrazioni sono solitamente presentate come strutture dati definite induttivamente (ad esempio, liste o alberi), costruite secondo gli assiomi e le regole di inferenza del sistema logico. (it) Bewijstheorie is een tak van de wiskundige logica die bewijzen als formele wiskundige objecten opvat. Hierdoor kunnen bewijzen door middel van wiskundige technieken worden geanalyseerd. Bewijzen worden meestal gepresenteerd als inductief gedefinieerde algoritmen, 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 een van de vier zogenaamde pilaren van de grondslagen van de wiskunde.Bewijstheorie kan ook worden beschouwd als een tak van de , waarin de bewijstheoretische semantiek het belangrijkste is. Het hangt er (nl) Teoria dowodu – dział logiki matematycznej zajmujący się analizą pojęcia dowodu oraz możliwych sposobów używania go w rozważaniach matematycznych. Za ojca tej dziedziny uważa się Davida Hilberta, jednego z najwybitniejszych matematyków przełomu dziewiętnastego i dwudziestego wieku. (pl) Теория доказательств — раздел математической логики, представляющий доказательства в виде формальных математических объектов, осуществляя их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определённых структур данных, таких как списки и деревья, созданных в соответствии с аксиомами и правилами вывода формальных систем. Таким образом, теория доказательств является синтаксической, в отличие от семантической теории моделей. Вместе с теорией моделей, аксиоматической теорией множеств и теорией вычислений, теория доказательств является одним из так называемых «четырёх столпов» математики. Теория доказательств использует точное определение понятия доказательства при доказательстве невозможности доказательства того или иного предложения в рамках зад (ru) A teoria das provas, teoria da prova ou teoria da demonstração é um ramo importante da lógica matemática que representa provas como objetos matemáticos, facilitando sua análise por técnicas matemáticas. Provas são tipicamente representadas por estruturas de dados definidas indutivamente, como listas simples, listas encadeadas, árvores, cada uma construída de acordo com os axiomas e regras de inferência do sistema lógico. Consequentemente, a teoria da prova é de natureza sintática, em contraste com a teoria dos modelos que é de natureza semântica. Juntamente com a teoria dos modelos, e a teoria da computabilidade, a teoria da prova é um dos chamados quatro pilares dos fundamentos da matemática. É também importante na lógica filosófica, onde os interesses principais estão na ideia de uma se (pt) |
| rdfs:label | Proof theory (en) نظرية البرهان (ar) Teoria de la demostració (ca) Beweistheorie (de) Pruvteorio (eo) Teoría de la demostración (es) Théorie de la démonstration (fr) Teoria della dimostrazione (it) 증명 이론 (ko) 証明論 (ja) Bewijstheorie (nl) Teoria dowodu (pl) Teoria da prova (pt) Теория доказательств (ru) Bevisteori (sv) Теорія доведення (uk) 证明论 (zh) |
| owl:sameAs | freebase:Proof theory http://sw.cyc.com/concept/Mx4rvWRWVpwpEbGdrcN5Y29ycA yago-res:Proof theory wikidata:Proof theory dbpedia-af:Proof theory dbpedia-ar:Proof theory http://bn.dbpedia.org/resource/প্রমাণ_তত্ত্ব dbpedia-ca:Proof theory dbpedia-de:Proof theory dbpedia-eo:Proof theory dbpedia-es:Proof theory dbpedia-fa:Proof theory dbpedia-fr:Proof theory dbpedia-he:Proof theory http://hy.dbpedia.org/resource/Ապացույցների_տեսություն dbpedia-it:Proof theory dbpedia-ja:Proof theory dbpedia-ko:Proof theory http://my.dbpedia.org/resource/သက်သေပြချက်သီအိုရီ dbpedia-nl:Proof theory dbpedia-pl:Proof theory dbpedia-pt:Proof theory dbpedia-ru:Proof theory dbpedia-sv:Proof theory dbpedia-tr:Proof theory dbpedia-uk:Proof theory dbpedia-vi:Proof theory dbpedia-zh:Proof theory https://global.dbpedia.org/id/4zzk5 |
| prov:wasDerivedFrom | wikipedia-en:Proof_theory?oldid=1119036403&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Proof_theory |
| is dbo:academicDiscipline of | dbr:Ulrich_Kohlenbach dbr:Helmut_Schwichtenberg dbr:Valeria_de_Paiva |
| is dbo:knownFor of | dbr:Rohit_Jivanlal_Parikh dbr:Gaisi_Takeuti |
| is dbo:mainInterest of | dbr:Grigori_Mints dbr:Jeremy_Avigad |
| is dbo:wikiPageDisambiguates of | dbr:Proof |
| is dbo:wikiPageRedirects of | dbr:History_of_proof_theory dbr:Plug_and_chug dbr:Subformula_property dbr:Proof-theoretic dbr:Proof_theorist |
| is dbo:wikiPageWikiLink of | dbr:Calculus_ratiocinator dbr:Primitive_recursive_function dbr:Proof_(truth) dbr:Proof_complexity dbr:Proof_net dbr:Propositional_calculus dbr:Quantum_logic dbr:Rohit_Jivanlal_Parikh dbr:Elementary_function_arithmetic dbr:List_of_academic_fields dbr:Model_theory dbr:Mac_Lane_coherence_theorem dbr:Meta-ethics dbr:Metalogic dbr:Metamathematics dbr:Metatheorem dbr:Metatheory dbr:Proof_compression dbr:Typed_lambda_calculus dbr:David_Hilbert dbr:History_of_proof_theory dbr:John_von_Neumann dbr:Paul_Lorenzen dbr:Resolution_proof_reduction_via_local_context_rewriting dbr:Reverse_mathematics dbr:Richard_Zach dbr:Cut-elimination_theorem dbr:Dag_Prawitz dbr:Ulrich_Kohlenbach dbr:Double-negation_translation dbr:Independence_of_premise dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(I–Q) dbr:Intuitionistic_type_theory dbr:Kőnig's_lemma dbr:List_of_inventions_and_discoveries_by_women dbr:List_of_mathematical_theories dbr:List_of_multiple_discoveries dbr:Structural_proof_theory dbr:Combinatory_logic dbr:Computability_theory dbr:Consistency dbr:Craig_interpolation dbr:Analytic_proof dbr:Material_conditional dbr:Mathematical_logic dbr:Mathematics dbr:Mathematical_object dbr:Structural_rule dbr:Coherentism dbr:Ekeland's_variational_principle dbr:Gaisi_Takeuti dbr:Gentzen's_consistency_proof dbr:Georg_Kreisel dbr:George_Boolos dbr:Gerhard_Gentzen dbr:Glossary_of_areas_of_mathematics dbr:Glossary_of_computer_science dbr:Bounded_arithmetic dbr:Conservative_extension dbr:Constructive_set_theory dbr:Correctness_(computer_science) dbr:Theorem dbr:Theory dbr:Ordinal_analysis dbr:Plug_and_chug dbr:Andrzej_Grzegorczyk dbr:Anne_Sjerp_Troelstra dbr:Linear_logic dbr:Logic dbr:Ludics dbr:Subformula_property dbr:Hardy_hierarchy dbr:Primitive_recursive_arithmetic dbr:Pure_type_system dbr:Actual_infinity dbr:Admissible_rule dbr:Transaction_logic dbr:Truth dbr:Truth_value dbr:Wilhelm_Ackermann dbr:Future_of_mathematics dbr:Gödel's_completeness_theorem dbr:Japaridze's_polymodal_logic dbr:Katalin_Bimbó dbr:Lambda-mu_calculus dbr:Large_countable_ordinal dbr:Laws_of_Form dbr:Primitive_recursive_functional dbr:Abductive_reasoning dbr:Curry–Howard_correspondence dbr:First-order_logic dbr:Partition_of_a_set dbr:Dialectica_interpretation dbr:Dialogical_logic dbr:Dick_de_Jongh dbr:Discrete_mathematics dbr:Fast-growing_hierarchy dbr:Formal_language dbr:Formal_proof dbr:Formation_rule dbr:Foundations_of_mathematics dbr:Hilbert's_paradox_of_the_Grand_Hotel dbr:Hilbert's_program dbr:Hilbert's_twenty-fourth_problem dbr:History_of_logic dbr:Logical_consequence dbr:Logical_disjunction dbr:Natural_deduction dbr:Mathematical_proof dbr:Proof dbr:Proof_procedure dbr:Provable dbr:Grigori_Mints dbr:Gödel's_incompleteness_theorems dbr:Helmut_Schwichtenberg dbr:Hilbert's_problems dbr:Atomic_formula dbr:Ivor_Grattan-Guinness dbr:Jaco_de_Bakker dbr:Jacques_Herbrand dbr:Jan_Śleszyński dbr:Jean-Yves_Girard dbr:Hybrid_logic dbr:Arnon_Avron dbr:Jeremy_Avigad dbr:Johan_van_Benthem_(logician) dbr:John_Corcoran_(logician) dbr:Lambda_calculus dbr:T._M._Scanlon dbr:Coherent_space dbr:Effective_results_in_number_theory dbr:Heyting_arithmetic dbr:Realizability dbr:Martin_Löb dbr:Philosophy_of_mathematics dbr:Frege_system dbr:If_and_only_if dbr:Kurt_Gödel dbr:Kurt_Schütte dbr:Method_of_analytic_tableaux dbr:Second-order_logic dbr:Sergei_N._Artemov dbr:Sequent_calculus dbr:Martin_Hyland dbr:Mathematics_Subject_Classification dbr:Sequent dbr:Turnstile_(symbol) dbr:Sara_Negri dbr:Extension_by_definitions dbr:Implicit_computational_complexity dbr:List_of_theorems dbr:Literal_(mathematical_logic) dbr:Self-verifying_theories dbr:Objections_to_evolution dbr:Richard_Bornat dbr:Proof_mining dbr:Walter_Carnielli dbr:Stanisław_Jaśkowski dbr:Richard's_paradox dbr:Verifiable_computing dbr:Setoid dbr:Valeria_de_Paiva dbr:Outline_of_academic_disciplines dbr:Outline_of_formal_science dbr:Outline_of_logic dbr:Outline_of_mathematics dbr:Slow-growing_hierarchy dbr:Takeuti–Feferman–Buchholz_ordinal dbr:Proof-theoretic dbr:Proof_theorist |
| is dbp:field of | dbr:Ulrich_Kohlenbach dbr:Helmut_Schwichtenberg |
| is dbp:mainInterests of | dbr:Grigori_Mints dbr:Jeremy_Avigad |
| is foaf:primaryTopic of | wikipedia-en:Proof_theory |