In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way that knowledge of the realizer gives knowledge about the truth of the formula. There are many variations of realizability; exactly which class of formulas is studied and which objects are realizers differ from one variation to another.
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - Réalisabilité (fr)
- 実現可能性 (論理学) (ja)
- Realizability (en)
- Realizabilidade (pt)
- 可实现性 (zh)
|
| rdfs:comment
| - 数理論理学において実現可能性（realizability）とは、構成的証明から追加情報を抽出するために使用される方法の集まりである。形式理論の論理式は「実現子」（realizer）と呼ばれるオブジェクトによって「実現」され、実現子の持つ情報が論理式の真理値についての情報を提供する。実現可能性には多くのバリエーションがあり、どの論理式のクラスが研究され、どのようなオブジェクトが実現子であるかは、それらバリエーションごとに異なる。 実現可能性は、直観主義論理のの形式化と見なせる。実現可能性を考えるとき、「証明」についての観念（BHK解釈では未定義のまま）は「実現子」についての形式的な観念に置き換えられる。ほとんどのバリエーションにおいて実現可能性は、研究対象の形式体系で証明可能なステートメントはすべて実現可能であるという定理から始まる。ただし、実現子は論理式について通常、形式的証明が直接提供するよりも多くの情報を提供する。 実現可能性は、直観主義的証明可能性への洞察を与えるだけでなく、直観主義理論におけると（英語: Disjunction and existence properties）の証明や、プルーフマイニングのように証明からプログラムの抽出のために適用できる。また、実現可能性トポス（realizability topos）を介したトポス理論とも関連している。 (ja)
- 可实现性是可用来处理关于公式的信息而不是关于公式的证明的那部分证明论。自然数n被称为实现了自然数算术的语言中一个陈述。其他逻辑和数学陈述也是可实现的，假如提供了解释合式公式一种方法，而不用借助达成这些公式的证明。 (zh)
- La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l' (en) par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard. (fr)
- In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way that knowledge of the realizer gives knowledge about the truth of the formula. There are many variations of realizability; exactly which class of formulas is studied and which objects are realizers differ from one variation to another. (en)
- Na lógica matemática, Realizabilidade é uma coleção de métodos na teoria da prova usado para estudar provas construtivas e extrair informações adicionais dele. Fórmulas de uma teoria formal são "compreendidas" como objetos, conhecidos como "realizadores", de um jeito que conhecimento do realizador dão conhecimento sobre a verdade da fórmula. Existem diversas variantes da Realizabilidade; exatamente que classe de fórmulas é estudada e que objetos são realizadores é o que distingue essas variantes. (pt)
|
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| has abstract
| - La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l' (en) par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard. Étant donnés une formule et un programme on note la propriété « réalise » ; cette notation est réminiscente du forcing de Cohen avec lequel la réalisabilité présente des analogies formelles. La réalisabilité conduit à une interprétation des formules comme des spécifications de programme : par exemple la tautologie est réalisée par les programmes qui étant donnée une entrée de type rendent un résultat de type . (fr)
- In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way that knowledge of the realizer gives knowledge about the truth of the formula. There are many variations of realizability; exactly which class of formulas is studied and which objects are realizers differ from one variation to another. Realizability can be seen as a formalization of the BHK interpretation of intuitionistic logic; in realizability the notion of "proof" (which is left undefined in the BHK interpretation) is replaced with a formal notion of "realizer". Most variants of realizability begin with a theorem that any statement that is provable in the formal system being studied is realizable. The realizer, however, usually gives more information about the formula than a formal proof would directly provide. Beyond giving insight into intuitionistic provability, realizability can be applied to prove the disjunction and existence properties for intuitionistic theories and to extract programs from proofs, as in proof mining. It is also related to topos theory via the . (en)
- 数理論理学において実現可能性（realizability）とは、構成的証明から追加情報を抽出するために使用される方法の集まりである。形式理論の論理式は「実現子」（realizer）と呼ばれるオブジェクトによって「実現」され、実現子の持つ情報が論理式の真理値についての情報を提供する。実現可能性には多くのバリエーションがあり、どの論理式のクラスが研究され、どのようなオブジェクトが実現子であるかは、それらバリエーションごとに異なる。 実現可能性は、直観主義論理のの形式化と見なせる。実現可能性を考えるとき、「証明」についての観念（BHK解釈では未定義のまま）は「実現子」についての形式的な観念に置き換えられる。ほとんどのバリエーションにおいて実現可能性は、研究対象の形式体系で証明可能なステートメントはすべて実現可能であるという定理から始まる。ただし、実現子は論理式について通常、形式的証明が直接提供するよりも多くの情報を提供する。 実現可能性は、直観主義的証明可能性への洞察を与えるだけでなく、直観主義理論におけると（英語: Disjunction and existence properties）の証明や、プルーフマイニングのように証明からプログラムの抽出のために適用できる。また、実現可能性トポス（realizability topos）を介したトポス理論とも関連している。 (ja)
- Na lógica matemática, Realizabilidade é uma coleção de métodos na teoria da prova usado para estudar provas construtivas e extrair informações adicionais dele. Fórmulas de uma teoria formal são "compreendidas" como objetos, conhecidos como "realizadores", de um jeito que conhecimento do realizador dão conhecimento sobre a verdade da fórmula. Existem diversas variantes da Realizabilidade; exatamente que classe de fórmulas é estudada e que objetos são realizadores é o que distingue essas variantes. Realizabilidade pode ser vista como a formalização da da lógica intuicionista; na Realizabilidade a noção de prova (que é deixada indefinida na interpretação BHK) é recolocada com uma notação formal de 'realizadores'. A maioria das variações da Realizabilidade começam com o teorema de que qualquer afirmação que é provada em um sistema formal estudado é realizável. O 'realizador', de qualquer maneira, geralmente dá mais informações sobre a fórmula do que a prova formal proveria. Além de dar uma visão sobre a demonstrabilidade intuicionista, Realizabilidade pode ser aplicada para provar a para teorias intuicionistas e para extrair programas de provas, como na . É também relacionado com a através da . (pt)
- 可实现性是可用来处理关于公式的信息而不是关于公式的证明的那部分证明论。自然数n被称为实现了自然数算术的语言中一个陈述。其他逻辑和数学陈述也是可实现的，假如提供了解释合式公式一种方法，而不用借助达成这些公式的证明。 (zh)
|
| gold:hypernym
| |
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage redirect
of | |
| is known for
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)