In mathematical logic, the cut rule is an inference rule of sequent calculus. It is a generalisation of the classical modus ponens inference rule. Its meaning is that, if a formula A appears as a conclusion in one proof and a hypothesis in another, then another proof in which the formula A does not appear can be deduced. In the particular case of the modus ponens, for example occurrences of man are eliminated of Every man is mortal, Socrates is a man to deduce Socrates is mortal.
Attributes | Values |
---|
rdf:type
| |
rdfs:label
| - Cut rule (en)
- Règle de coupure (fr)
- Regra do corte (pt)
- Сечение (теория доказательств) (ru)
|
rdfs:comment
| - In mathematical logic, the cut rule is an inference rule of sequent calculus. It is a generalisation of the classical modus ponens inference rule. Its meaning is that, if a formula A appears as a conclusion in one proof and a hypothesis in another, then another proof in which the formula A does not appear can be deduced. In the particular case of the modus ponens, for example occurrences of man are eliminated of Every man is mortal, Socrates is a man to deduce Socrates is mortal. (en)
- En logique mathématique, la règle de coupure est une règle d'inférence du calcul des séquents, qui généralise le modus ponens. Sa signification est que, si une formule A apparaît comme conclusion dans un séquent et comme hypothèse dans un autre, on peut alors inférer un séquent dans lequel la formule A n'apparaît pas. (fr)
- Сечение в теории доказательств — правило вывода, позволяющее удалить («высечь») промежуточное высказывание : . Поскольку правило сечения не обладает (требующим, чтобы посылки состояли из подформул заключения), особую значимость (в том числе для возможности конструктивного доказательства их непротиворечивости) приобретают логические исчисления с устранимостью сечений, то есть такие, в которых всякую выводимую секвенцию можно вывести без сечения. Для классического и интуиционистского исчислений секвенций свойство доказано Генценом, в дальнейшем оно установлено для большой серии классических и неклассических теорий высших порядков. (ru)
- Em lógica matemática, a regra do corte é uma regra de inferência do cálculo de sequentes. É uma generalização da regra de inferência clássica modus ponens. Seu significado é o de que, se uma fórmula A é apresentada como uma conclusão em uma prova e como uma hipótese em outra prova, então uma terceira prova em que a fórmula A não aparece pode ser deduzida. No caso particular do modus ponens, por exemplo, as ocorrências de homem são eliminadas de Todo homem é mortal, Sócrates é um homem para se deduzir Sócrates é mortal. (pt)
|
dcterms:subject
| |
Wikipage page ID
| |
Wikipage revision ID
| |
Link from a Wikipage to another Wikipage
| |
sameAs
| |
dbp:wikiPageUsesTemplate
| |
has abstract
| - In mathematical logic, the cut rule is an inference rule of sequent calculus. It is a generalisation of the classical modus ponens inference rule. Its meaning is that, if a formula A appears as a conclusion in one proof and a hypothesis in another, then another proof in which the formula A does not appear can be deduced. In the particular case of the modus ponens, for example occurrences of man are eliminated of Every man is mortal, Socrates is a man to deduce Socrates is mortal. (en)
- En logique mathématique, la règle de coupure est une règle d'inférence du calcul des séquents, qui généralise le modus ponens. Sa signification est que, si une formule A apparaît comme conclusion dans un séquent et comme hypothèse dans un autre, on peut alors inférer un séquent dans lequel la formule A n'apparaît pas. (fr)
- Сечение в теории доказательств — правило вывода, позволяющее удалить («высечь») промежуточное высказывание : . Поскольку правило сечения не обладает (требующим, чтобы посылки состояли из подформул заключения), особую значимость (в том числе для возможности конструктивного доказательства их непротиворечивости) приобретают логические исчисления с устранимостью сечений, то есть такие, в которых всякую выводимую секвенцию можно вывести без сечения. Для классического и интуиционистского исчислений секвенций свойство доказано Генценом, в дальнейшем оно установлено для большой серии классических и неклассических теорий высших порядков. (ru)
- Em lógica matemática, a regra do corte é uma regra de inferência do cálculo de sequentes. É uma generalização da regra de inferência clássica modus ponens. Seu significado é o de que, se uma fórmula A é apresentada como uma conclusão em uma prova e como uma hipótese em outra prova, então uma terceira prova em que a fórmula A não aparece pode ser deduzida. No caso particular do modus ponens, por exemplo, as ocorrências de homem são eliminadas de Todo homem é mortal, Sócrates é um homem para se deduzir Sócrates é mortal. (pt)
|
gold:hypernym
| |
prov:wasDerivedFrom
| |
page length (characters) of wiki page
| |
foaf:isPrimaryTopicOf
| |
is Link from a Wikipage to another Wikipage
of | |
is foaf:primaryTopic
of | |