| dbo:abstract
|
- Systeme (oder Kalküle) natürlichen Schließens bezeichnen in der mathematischen und philosophischen Logik einen Kalkültyp, der 1934 von Gerhard Gentzen und etwa zeitgleich von Stanisław Jaśkowski – einem Vertreter der Lemberg-Warschau-Schule – entwickelt wurde. Der Begriff des Kalküls des natürlichen Schließens (KdnS) ist nicht streng definiert, stattdessen gibt es eine Reihe von Merkmalen, die auf KdnS in unterschiedlichem Maße zutreffen und dabei bestimmen, wie typisch das Exemplar für die Gattung ist.
* Anders als bei den allermeisten anderen Kalkültypen wie Tableaukalkül, Axiomatischem Kalkül, Dialogkalkül etc. gibt es im KdnS die Möglichkeit, Aussagen anzunehmen, die für eine Weile innerhalb der Ableitung ihre Gültigkeit haben. Diese Annahmen können später wieder getilgt werden (siehe dazu auch unten). Dieses Merkmal macht einen großen Anteil an der „Natürlichkeit“ des Schließens im KdnS aus, denn es entspricht der gängigen Praxis in mathematischen Beweisen.
* Im Gegensatz zu axiomatischen Kalkülen enthält ein System natürlichen Schließens keine bzw. kaum Axiome, sondern hauptsächlich eine größere Zahl von Schlussregeln. Zusammen mit den gleichfalls von Gentzen entwickelten Sequenzenkalkülen gehören Systeme des natürlichen Schließens deshalb zur Familie der Regellogiken oder Regelkalküle.
* Die Schlussregeln in einem KdnS sollten intuitiv zu rechtfertigen sein, am besten prätheoretisch akzeptierten Beweistechniken entsprechen. Auch dieses Merkmal trägt zur „Natürlichkeit“ des Schließens bei.
* Üblicherweise werden die Schlussregeln so systematisiert, dass für jeden logischen Operator (Junktor bzw. Quantor) eine Einführungs- und eine Beseitigungsregel angegeben ist. Die Einführungsregel für einen Operator O erlaubt es, zu einer Aussage mit O als Hauptoperator überzugehen; die Beseitigungsregel führt von einer Aussage mit O als Hauptoperator zu einer anderen Aussage. Aufgrund der Natürlichkeit des Schließens und der Systematisierung in Einführungs- und Beseitigungsregeln lässt sich mit einem KdnS der Anspruch einer „beweistheoretischen Semantik“ verbinden, welche die Bedeutung der logischen Operatoren durch die Angabe von Schlussregeln festlegen will. (de)
- La deducción natural es una aproximación a la teoría de la demostración en la que se busca capturar la manera en que las personas razonan naturalmente al construir demostraciones matemáticas. En vez de contar con unos pocos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone vaciar la lista de axiomas y ampliar la de reglas de inferencia, introduciendo dos reglas para cada constante lógica: una para introducirla y otra para eliminarla. Una demostración se construye partiendo de supuestos y aplicando las reglas para llegar a la conclusión deseada.Sirve para demostrar la validez de un argumento. La deducción natural fue introducida por Gerhard Gentzen en su trabajo Investigaciones sobre la inferencia lógica (Untersuchungen über das logische Schliessen), publicado en 1934-1935. (es)
- En logique mathématique, la déduction naturelle est un système formel où les règles de déduction des démonstrations sont proches des façons naturelles de raisonner. C'est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons :
* contrairement aux systèmes à la Hilbert fondés sur des listes d'axiomes logiques plus ou moins ad hoc, la déduction naturelle repose sur un principe systématique de symétrie : pour chaque connecteur, on donne une paire de règles duales (introduction/élimination) ;
* elle a conduit Gentzen à inventer un autre formalisme très important en théorie de la démonstration, encore plus « symétrique » : le calcul des séquents ;
* elle a permis dans les années 1960 d'identifier la première instance de l'isomorphisme de Curry-Howard. La terminologie « déduction naturelle » a été suggérée, par Gentzen, eu égard à l'aspect peu intuitif des systèmes à la Hilbert. (fr)
- In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning. (en)
- 自然演繹（しぜんえんえき、英: Natural deduction）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。 (ja)
- 논리학 및 증명이론에서 자연 연역(自然演繹, natural deduction)이란 자연스러운 논리적 추론을 나타내는 증명 연산의 일종으로, 최대한 공리를 배제하고 오직 구문적인 추론 규칙만을 사용한 증명이 이루어지는 것이 특징이다. 이는, 추론규칙의 논리적 법칙을 표현하기 위해 많은 공리들을 이용하는 힐베르트 체계와는 대조된다. (ko)
- Natuurlijke deductie is een methode om via deductie met noodzakelijkheid de geldigheid van een redenering conform vastgestelde regels te bewijzen in de logica. Het model zou gebaseerd zijn op een "natuurlijke" vorm van redeneren. Systemen van natuurlijke deductie zijn ontwikkeld voor verschillende vormen van logica, waaronder de propositielogica en de predicaatlogica. (nl)
- Dedukcja naturalna – bardzo intuicyjny i generujący dowody system dowodzenia twierdzeń, bazujący na systemach Hilberta. Dowód to lista formuł objętych oknami. Operacje w bardzo prostej wersji to:
* dodanie założenia, otwiera to okno,
* przepisanie dowolnego aktywnego założenia,
* zamknięcie okna, dodaje się za oknem formułę „pierwsza formuła okna ostatnia formuła okna”, wszystkie formuły w oknie są dezaktywowane,
* użycie jednej z reguł dowodzenia (w szczególności modus ponens na dowolnych aktywnych) na dowolnych aktywnych formułach. Każda formuła leżąca poza oknem, zwykle powstała w wyniku zamknięcia ostatniego okna, jest twierdzeniem. Okna są wyłącznie graficzną reprezentacją tego co się dzieje. (pl)
- La deduzione naturale è, nel campo della logica, un sistema deduttivo. Un sistema deduttivo è una relazione che può sussistere tra un insieme di formule e una formula: se la relazione vale, diciamo che la formula viene dedotta dall'insieme. La deduzione naturale si propone quindi come un metodo per dimostrare che un'affermazione è conseguenza di certe ipotesi. A differenza dei sistemi assiomatici è un sistema senza assiomi, basato su una serie di regole di inferenza il cui numero dipende dai connettivi che definiamo come primitivi. (it)
- Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Foram introduzidos pela primeira vez, nos anos 30, por Gentzen.Para poder realizar uma derivação formal, é necessário formalizar a expressão que queremos demonstrar. Formalizar significa traduzir da forma linguística usual para uma notação lógica, uma forma que é entendível para qualquer um, independente da língua que fala, e que também reduz o espaço ocupado pela frase escrita, tendo em vista que podemos utilizar uma notação mais económica, a lógica. Na notação formal utilizamos conectivos lógicos, operadores que realizam a ligação entre os átomos (os menores objetos). São eles:
* - Negação (não é um conectivo, simplesmente nega a fórmula ou átomo ligado)
* - Conjunção
* - Disjunção
* - Implicação
* - Bi-implicação No caso da lógica clássica de primeira ordem, temos ainda os quantificadores:
* - Universal
* - Existencial Também utilizamos alguns símbolos extras para auxiliar:
* - Derivação
* - Consequência semântica
* - Top (Verdade)
* - Bottom (Absurdo, falsidade) (pt)
- 在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。 (zh)
|
| rdfs:comment
|
- In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning. (en)
- 自然演繹（しぜんえんえき、英: Natural deduction）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。 (ja)
- 논리학 및 증명이론에서 자연 연역(自然演繹, natural deduction)이란 자연스러운 논리적 추론을 나타내는 증명 연산의 일종으로, 최대한 공리를 배제하고 오직 구문적인 추론 규칙만을 사용한 증명이 이루어지는 것이 특징이다. 이는, 추론규칙의 논리적 법칙을 표현하기 위해 많은 공리들을 이용하는 힐베르트 체계와는 대조된다. (ko)
- Natuurlijke deductie is een methode om via deductie met noodzakelijkheid de geldigheid van een redenering conform vastgestelde regels te bewijzen in de logica. Het model zou gebaseerd zijn op een "natuurlijke" vorm van redeneren. Systemen van natuurlijke deductie zijn ontwikkeld voor verschillende vormen van logica, waaronder de propositielogica en de predicaatlogica. (nl)
- La deduzione naturale è, nel campo della logica, un sistema deduttivo. Un sistema deduttivo è una relazione che può sussistere tra un insieme di formule e una formula: se la relazione vale, diciamo che la formula viene dedotta dall'insieme. La deduzione naturale si propone quindi come un metodo per dimostrare che un'affermazione è conseguenza di certe ipotesi. A differenza dei sistemi assiomatici è un sistema senza assiomi, basato su una serie di regole di inferenza il cui numero dipende dai connettivi che definiamo come primitivi. (it)
- 在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。 (zh)
- Systeme (oder Kalküle) natürlichen Schließens bezeichnen in der mathematischen und philosophischen Logik einen Kalkültyp, der 1934 von Gerhard Gentzen und etwa zeitgleich von Stanisław Jaśkowski – einem Vertreter der Lemberg-Warschau-Schule – entwickelt wurde. Der Begriff des Kalküls des natürlichen Schließens (KdnS) ist nicht streng definiert, stattdessen gibt es eine Reihe von Merkmalen, die auf KdnS in unterschiedlichem Maße zutreffen und dabei bestimmen, wie typisch das Exemplar für die Gattung ist. (de)
- La deducción natural es una aproximación a la teoría de la demostración en la que se busca capturar la manera en que las personas razonan naturalmente al construir demostraciones matemáticas. En vez de contar con unos pocos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone vaciar la lista de axiomas y ampliar la de reglas de inferencia, introduciendo dos reglas para cada constante lógica: una para introducirla y otra para eliminarla. Una demostración se construye partiendo de supuestos y aplicando las reglas para llegar a la conclusión deseada.Sirve para demostrar la validez de un argumento. (es)
- En logique mathématique, la déduction naturelle est un système formel où les règles de déduction des démonstrations sont proches des façons naturelles de raisonner. C'est une étape importante de l'histoire de la théorie de la démonstration pour plusieurs raisons : La terminologie « déduction naturelle » a été suggérée, par Gentzen, eu égard à l'aspect peu intuitif des systèmes à la Hilbert. (fr)
- Dedukcja naturalna – bardzo intuicyjny i generujący dowody system dowodzenia twierdzeń, bazujący na systemach Hilberta. Dowód to lista formuł objętych oknami. Operacje w bardzo prostej wersji to:
* dodanie założenia, otwiera to okno,
* przepisanie dowolnego aktywnego założenia,
* zamknięcie okna, dodaje się za oknem formułę „pierwsza formuła okna ostatnia formuła okna”, wszystkie formuły w oknie są dezaktywowane,
* użycie jednej z reguł dowodzenia (w szczególności modus ponens na dowolnych aktywnych) na dowolnych aktywnych formułach. (pl)
- Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Foram introduzidos pela primeira vez, nos anos 30, por Gentzen.Para poder realizar uma derivação formal, é necessário formalizar a expressão que queremos demonstrar. Formalizar significa traduzir da forma linguística usual para uma notação lógica, uma forma que é entendível para qualquer um, independente da língua que fala, e que também reduz o espaço ocupado pela frase escrita, tendo em vista que podemos utilizar uma notação mais económica, a lógica.
* - Universal
* - Existencial (pt)
|
