About: Proof theory

An Entity of Type: organisation, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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 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.

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)
  • 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)
  • 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 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)
  • 証明論(しょうめいろん、英語: proof theory)は、数理論理学の一分野であり、証明を数学的対象として形式的に表し、それに数学的解析を施す。 (ja)
  • 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 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. 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)
  • 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)
  • 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)
  • Теория доказательств — раздел математической логики, представляющий доказательства в виде формальных математических объектов, осуществляя их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определённых структур данных, таких как списки и деревья, созданных в соответствии с аксиомами и правилами вывода формальных систем. Таким образом, теория доказательств является синтаксической, в отличие от семантической теории моделей. Вместе с теорией моделей, аксиоматической теорией множеств и теорией вычислений, теория доказательств является одним из так называемых «четырёх столпов» математики. Теория доказательств использует точное определение понятия доказательства при доказательстве невозможности доказательства того или иного предложения в рамках заданной математической теории. Теория доказательств важна для философской логики, где самостоятельный интерес представляет идея теоретико-доказательственной семантики, — идея, которая основана на осуществимости формально-логических методов структурной теории доказательств. (ru)
  • 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)
  • Teoria da prova é um ramo 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. 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.A teoria da prova é 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. (pt)
  • Теорія доведення (доказів) є розділом математичної логіки, який представляє докази у вигляді формальних математичних об'єктів, здійснюючи їх аналіз за допомогою математичних методів. Докази, як правило, представлені у вигляді індуктивно визначеної структури даних, таких як списки і дерева, створених відповідно до аксіом і правил виводу формальних систем. Таким чином, теорія доказів є синтаксичною, на відміну від семантичної теорії моделей. Разом з теорією моделей, аксіоматичною теорією множин та теорією обчислень, теорія доказів є одним з так званих «чотирьох стовпів» основ математики. (uk)
  • 证明论是数理逻辑的一个分支,它将数学证明表达为形式化的数学客体,从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达,例如链表,盒链表,或者树,它们根据逻辑系统的公理和推理规则构造。因此,证明论本质上是语法逻辑,和本质上是语义学的模型论形相反。和模型论,公理化集合论,以及递归论一起,证明论被称为数学基础的四大支柱之一。 证明论也可视为哲学逻辑的分支,其主要兴趣在于的思想,该思想依赖于的技术型想法才可行。 (zh)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 183478 (xsd:integer)
dbo:wikiPageLength
  • 19479 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1001008528 (xsd:integer)
dbo:wikiPageWikiLink
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
dct:subject
gold:hypernym
rdf:type
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)
  • 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)
  • 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 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)
  • 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)
  • 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)
  • Teoria da prova é um ramo 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. 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.A teoria da prova é 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 (pt)
  • Теория доказательств — раздел математической логики, представляющий доказательства в виде формальных математических объектов, осуществляя их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определённых структур данных, таких как списки и деревья, созданных в соответствии с аксиомами и правилами вывода формальных систем. Таким образом, теория доказательств является синтаксической, в отличие от семантической теории моделей. Вместе с теорией моделей, аксиоматической теорией множеств и теорией вычислений, теория доказательств является одним из так называемых «четырёх столпов» математики. Теория доказательств использует точное определение понятия доказательства при доказательстве невозможности доказательства того или иного предложения в рамках зад (ru)
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)
  • 証明論 (ja)
  • Teoria della dimostrazione (it)
  • 증명 이론 (ko)
  • Bewijstheorie (nl)
  • Teoria dowodu (pl)
  • Teoria da prova (pt)
  • Bevisteori (sv)
  • Теория доказательств (ru)
  • Теорія доведення (uk)
  • 证明论 (zh)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:academicDiscipline of
is dbo:knownFor of
is dbo:mainInterest of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:field of
is dbp:mainInterests of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License