This HTML5 document contains 157 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbthttp://dbpedia.org/resource/Template:
wikipedia-enhttp://en.wikipedia.org/wiki/
n4https://web.archive.org/web/20060925141642/http:/www.pps.jussieu.fr/~dicosmo/
dbrhttp://dbpedia.org/resource/
n28http://girard.perso.math.cnrs.fr/
n30http://www.csl.sri.com/users/lincoln/
n21http://llwiki.ens-lyon.fr/
n7http://www.lix.polytechnique.fr/Labo/Dale.Miller/
dbpedia-frhttp://fr.dbpedia.org/resource/
dctermshttp://purl.org/dc/terms/
n32http://www.csl.sri.com/~lincoln/papers/
n31http://www.dicosmo.org/CourseNotes/LinLog/
dbpedia-cshttp://cs.dbpedia.org/resource/
rdfshttp://www.w3.org/2000/01/rdf-schema#
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n35https://web.archive.org/web/20160704202340/http:/www.cs.man.ac.uk/~pt/stable/
dbphttp://dbpedia.org/property/
xsdhhttp://www.w3.org/2001/XMLSchema#
n24http://plato.stanford.edu/entries/logic-linear/
dbohttp://dbpedia.org/ontology/
n11http://homepages.inf.ed.ac.uk/wadler/topics/
dbpedia-pthttp://pt.dbpedia.org/resource/
n36http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/
dbpedia-jahttp://ja.dbpedia.org/resource/
dbchttp://dbpedia.org/resource/Category:
dbpedia-ruhttp://ru.dbpedia.org/resource/
wikidatahttp://www.wikidata.org/entity/
n17http://www.brics.dk/LS/96/6/
goldhttp://purl.org/linguistics/gold/
n37https://global.dbpedia.org/id/
dbpedia-ithttp://it.dbpedia.org/resource/
provhttp://www.w3.org/ns/prov#
n13http://bach.istc.kobe-u.ac.jp/llprover/
foafhttp://xmlns.com/foaf/0.1/
dbpedia-zhhttp://zh.dbpedia.org/resource/
dbpedia-kohttp://ko.dbpedia.org/resource/
dbpedia-eshttp://es.dbpedia.org/resource/
freebasehttp://rdf.freebase.com/ns/
owlhttp://www.w3.org/2002/07/owl#

Statements

Subject Item
dbr:Linear_logic
rdf:type
owl:Thing
rdfs:label
선형 논리 线性逻辑 Logica lineare Линейная логика Linear logic Lógica linear 線形論理 Lineární logika Lógica lineal Logique linéaire
rdfs:comment
在数理逻辑中，线性逻辑是拒绝“弱化”和“收缩”的结构规则的一种亚结构逻辑。对此解释是“假设是资源”:在证明中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如经典逻辑或直觉逻辑，那里统治判断是“真理”，它可以按需要被自由的使用多次。例如，从命题A和A ⇒ B能按如下步骤得出结果A ∧ B: 1. * （1）在假定A和A ⇒ B上应用肯定前件（或蕴涵除去）得到结论B。 2. * （2）A和（1）的合取的得到结论A ∧ B。 这经常被符号化表示为相继式：A, A ⇒ B B。在上述证明中"消费"了A为真的事实；这种真理的"自由"通常是在形式化数学中所需要的。 但是，真理经常在应用于关于这个世界的陈述的时候太抽象或不实用。比如，假设我有一夸脱的牛奶，我能用它制作一磅奶酪。如果我决定把我的所有牛奶都制成奶酪，我就不能下结论说我有牛奶和奶酪二者! 上面的逻辑模式让我们得到结论：牛奶, 牛奶⇒奶酪牛奶∧奶酪（这里的牛奶表示命题"我有一夸脱牛奶"，等等）。普通逻辑建模这个活动失败是由于牛奶、奶酪一般是资源：资源的数量不像真理是可以随意使用和支配的自由事实，而是必须在所有"状态变更"中仔细计量的。关于牛奶制奶酪活动的准确陈述是： 从一夸脱牛奶和从一夸脱牛奶转换出一磅奶酪的过程，我们获得一磅奶酪。 在线性逻辑中我们写为：牛奶, 牛奶奶酪奶酪，使用了不同的连结词（替代了⇒）和不同的逻辑蕴涵符号。 Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics (because linear logic can be seen as the logic of quantum information theory), as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction. La logica lineare è una proposta da come un raffinamento della logica classica ed intuizionista, coniugando le dualità che caratterizzano i connettivi della prima con le proprietà costruttive della seconda. Sebbene questo sistema logico sia un oggetto di studio fine a se stesso, più in generale le idee della logica lineare hanno influito in settori come i linguaggi di programmazione, la o la fisica dei quanti e la linguistica, in particolare per la sua enfasi sulle risorse limitate, la dualità e l'interazione. Линейная логика (англ. Linear Logic — это подструктурная логика, предложенная (англ. Jean-Yves Girard) как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней, введена и используется для логических рассуждений, учитывающих расход некоторого ресурса. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации), лингвистика. En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire, inventée par le logicien Jean-Yves Girard en 1986, est un système formel qui, du point de vue logique, décompose et analyse les logiques classique et intuitionniste et, du point de vue calculatoire, est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources. 선형 논리(Linear logic)는 장-이브 지라르(Jean-Yves Girard)가 고전 및 직관 논리의 개선으로 제안한 하위 구조 논리로 전자의 쌍대성을 후자의 구성주의적 속성과 결합한다. 논리학도 그 자체로 연구되었지만, 보다 넓게는 선형 논리학의 아이디어가 프로그래밍 언어, 게임 의미론, 양자 물리학, 언어학 같은 분야에 영향을 미쳤다. (선형 논리는 양자 정보 이론 의 논리라고 볼 수 있기 때문이다.) 선형 논리는 다양한 프레젠테이션, 설명 및 직관에 적합하다. 증명 이론상, 그것은 시퀀트 계산의 분석에서 파생된다. 이것은 논리적 추론이 더 이상 계속해서 확장되는 지속적인 "진리"의 모음에 관한 것이 아니라, 마음대로 복제하거나 버릴 수 없는 자원을 조작하는 방법이라는 것을 의미한다. 단순 표시적 의미론 관점에서 선형 논리는 데카르트 닫힌 범주를 대칭 모노이드 범주로 대체하거나 불 대수를 C*-대수로 대체하여 고전 논리의 해석을 개선하는 것으로 볼 수 있다. 고전 선형 논리 (CLL)의 언어는 BNF 표기법에 의해 귀납적으로 정의된다. 여기서 p 및 p⊥ 는 논리적 원자 범위이다. 다음 용어를 추가로 사용할 수 있다. La lógica lineal es un proceso analítico cuyo orden es invariable, y donde no se aceptan errores. Se puede comprender de forma lógica como un perfeccionamiento de determinadas operaciones lógicas cuando el número de veces que una hipótesis es usada para un razonamiento es de vital importancia. Las propiedades de las proposiciones de esta lógica, muestran que su naturaleza es dinámica. Existen varios tipos de conectores lineales: * Conjunción aditiva (A&B) * Conjunción multiplicativa (A⊗B) * Implicación lineal (A-->B) * Datos: Q841728 * Multimedia: Linear logic / Q841728 Lineární logika je verze formální logiky, v níž při odvození dochází k vyřazení antecedentu z množiny formulí. Máme-li napříklada pravidlo (lineární implikaci),můžeme odvodit,tj. A "zmizí" a není již k dispozici pro další pravidla. Používá se zejména při zpracování přirozeného jazyka pro generování logické reprezentace vět (poprvé byla pro tuto úlohu použita v ).Například význam slovesa věty John loves Mary lze vyjádřit takto: 線形論理（せんけいろんり、英: Linear logic）は、「弱化(weakening)規則」と「縮約(contraction)規則」というを否定した部分構造論理の一種である。「資源としての仮説 (hypotheses as resources)」という解釈をする。すなわち、全ての仮説は証明において「一回だけ」消費される。古典論理や直観論理のような論理体系では、仮説（前提）は必要に応じて何度でも使える。例えば、A と A ⇒ B という命題から A ∧ B という結論を導出するのは、次のようになる。 1. * A と A ⇒ B を前提とするモーダスポネンス（あるいは自然演繹でいう含意の除去）により、B が得られる。 2. * 前提 A と (1) の論理積から A ∧ B が得られる。 これをシークエントで表すと、A, A ⇒ B ⊢ A ∧ B となる。上記の証明ではどちらの行でも、A が真であるという事実を「消費」している。この真理の「気軽さ」は形式手法では一般に必須である。 このような活動を通常の論理でうまく表せないのは、クリームやバターなどの「資源」全般の性質によるものである。ある量の資源は、真理のように好きなように使ったり始末したりできず、全ての「状態変化」について注意深く見ていかなければならない。バター作りを正確に表すと、次のようになる。 Lógica linear é um lógica subestrutural proposta por Jean-Yves Girard como um refinamento da lógica clássica e intuicionista, juntando as dualidades da primeira com muitas das propriedades construtivas da última. Embora a lógica também tenha sido estudada por si mesma, mais amplamente, as ideias da lógica linear têm influenciado em campos como linguagens de programação, jogos de semântica e física quântica, bem como a linguística, particularmente devido a sua ênfase na limitação de recursos, dualidade e interação.
rdfs:seeAlso
dbr:Quantale
dcterms:subject
dbc:Logic dbc:Substructural_logic dbc:Linear_logic dbc:Non-classical_logic
dbo:wikiPageID
579675
dbo:wikiPageRevisionID
1115771213
dbo:wikiPageWikiLink
dbr:Structural_rule dbr:NP-complete dbr:Substructural_logic dbr:Denotational_semantics dbr:Cartesian_closed_categories dbr:Logical_connective dbr:Logical_consequence dbr:Completeness_of_atomic_initial_sequents dbr:Intuitionistic_logic dbr:Lollipop dbr:Logical_harmony dbr:Boolean_algebras dbr:Logic_of_unity dbr:Admissible_rule dbr:First-order_logic dbr:Proof_theory dbr:Game_semantics dbr:Linguistics dbr:Canonical_form dbr:Tony_Hoare dbr:Petri_nets dbr:Horn_clauses dbr:Identity_element dbr:Gödel–Gentzen_negative_translation dbr:Cut-elimination_theorem dbr:Undecidable_problem dbr:Programming_languages dbr:Jean-Yves_Girard dbr:Quantum_physics dbr:Entailment dbr:Chu_space dbr:Logical_truth dbr:Idempotency_of_entailment dbc:Logic dbr:Classical_logic dbr:Lambda-calculus dbc:Substructural_logic dbr:Proof_net dbr:Normal_modal_logic dbr:EXPSPACE dbr:Relevant_logic dbr:PSPACE-complete dbr:Symmetric_monoidal_categories dbr:Substructural_type_system dbr:Sequent_calculus dbr:Logical_disjunction dbr:Backus–Naur_form dbr:Quantum_information_theory dbr:Affine_logic dbr:Logical_conjunction dbr:Linear_type_system dbr:Involution_(mathematics) dbr:Uniqueness_type dbr:Strict_logic dbr:Linear_logic_programming dbr:Ludics dbr:Atomic_formula dbr:Monotonicity_of_entailment dbr:Turnstile_(symbol) dbr:C*-algebras dbr:Noncommutative_logic dbr:De_Morgan's_laws dbc:Linear_logic dbr:Theoretical_Computer_Science_(journal) dbr:A._S._Troelstra dbr:Constructivism_(mathematics) dbc:Non-classical_logic dbr:Analytic_proof dbr:Computability_logic dbr:Duality_(mathematics) dbr:Frame_problem dbr:Exchange_rule dbr:Geometry_of_interaction dbr:Higher-order_logic
dbo:wikiPageExternalLink
n4:index.html.en n7: n11:linear-logic.html n13: n17:BRICS-LS-96-6.pdf n21: n24: n28:linear.pdf n30: n31: n32:sigact92.ps n35:Proofs+Types.html n36:llp.pdf
owl:sameAs
wikidata:Q841728 dbpedia-es:Lógica_lineal dbpedia-pt:Lógica_linear dbpedia-ru:Линейная_логика dbpedia-ja:線形論理 freebase:m.02s1gd dbpedia-zh:线性逻辑 dbpedia-ko:선형_논리 dbpedia-it:Logica_lineare dbpedia-fr:Logique_linéaire n37:4zVHe dbpedia-cs:Lineární_logika
dbp:wikiPageUsesTemplate
dbt:See_also dbt:Isbn dbt:Math dbt:Redirect dbt:= dbt:Tee dbt:Clarify dbt:Main dbt:Reflist dbt:Non-classical_logic dbt:Citation_needed dbt:Commons_category-inline dbt:Short_description dbt:Portal
dbp:date
May 2015
dbp:reason
It is difficult to guess what this might mean without a link
dbo:abstract
線形論理（せんけいろんり、英: Linear logic）は、「弱化(weakening)規則」と「縮約(contraction)規則」というを否定した部分構造論理の一種である。「資源としての仮説 (hypotheses as resources)」という解釈をする。すなわち、全ての仮説は証明において「一回だけ」消費される。古典論理や直観論理のような論理体系では、仮説（前提）は必要に応じて何度でも使える。例えば、A と A ⇒ B という命題から A ∧ B という結論を導出するのは、次のようになる。 1. * A と A ⇒ B を前提とするモーダスポネンス（あるいは自然演繹でいう含意の除去）により、B が得られる。 2. * 前提 A と (1) の論理積から A ∧ B が得られる。 これをシークエントで表すと、A, A ⇒ B ⊢ A ∧ B となる。上記の証明ではどちらの行でも、A が真であるという事実を「消費」している。この真理の「気軽さ」は形式手法では一般に必須である。 しかし、日常的な世界に関する文に適用するには、真理は抽象的すぎ、扱いにくい。例えば、約1リットルのクリームから約450グラムのバターができるとする。クリームをバターを作るのに使うとすると、クリームとバターの両方を持っているという結論は得られない。ところが上の論法でいけば cream, cream ⇒ butter ⊢ cream ∧ butter となる（ここで、cream は「私は1リットルのクリームを持っている」という命題を表し、butter は「私は450グラムのバターを持っている」という命題を表す）。 このような活動を通常の論理でうまく表せないのは、クリームやバターなどの「資源」全般の性質によるものである。ある量の資源は、真理のように好きなように使ったり始末したりできず、全ての「状態変化」について注意深く見ていかなければならない。バター作りを正確に表すと、次のようになる。 1リットルのクリームがあり、1リットルのクリームを450グラムのバターに変換するプロセスを経ると、450グラムのバターが得られる。 線形論理ではこれを cream, cream ⊸ butter ⊩ butter と表記する。論理結合子（⇒ の代わりに ⊸）と論理内含（⊢ の代わりに ⊩）の記号が異なる点に注意されたい。 線形論理は1987年、フランスの論理学者ジャン＝イヴ・ジラールが提唱した。 La lógica lineal es un proceso analítico cuyo orden es invariable, y donde no se aceptan errores. Se puede comprender de forma lógica como un perfeccionamiento de determinadas operaciones lógicas cuando el número de veces que una hipótesis es usada para un razonamiento es de vital importancia. Las propiedades de las proposiciones de esta lógica, muestran que su naturaleza es dinámica. Existen varios tipos de conectores lineales: * Conjunción aditiva (A&B) * Conjunción multiplicativa (A⊗B) * Implicación lineal (A-->B) * Datos: Q841728 * Multimedia: Linear logic / Q841728 선형 논리(Linear logic)는 장-이브 지라르(Jean-Yves Girard)가 고전 및 직관 논리의 개선으로 제안한 하위 구조 논리로 전자의 쌍대성을 후자의 구성주의적 속성과 결합한다. 논리학도 그 자체로 연구되었지만, 보다 넓게는 선형 논리학의 아이디어가 프로그래밍 언어, 게임 의미론, 양자 물리학, 언어학 같은 분야에 영향을 미쳤다. (선형 논리는 양자 정보 이론 의 논리라고 볼 수 있기 때문이다.) 선형 논리는 다양한 프레젠테이션, 설명 및 직관에 적합하다. 증명 이론상, 그것은 시퀀트 계산의 분석에서 파생된다. 이것은 논리적 추론이 더 이상 계속해서 확장되는 지속적인 "진리"의 모음에 관한 것이 아니라, 마음대로 복제하거나 버릴 수 없는 자원을 조작하는 방법이라는 것을 의미한다. 단순 표시적 의미론 관점에서 선형 논리는 데카르트 닫힌 범주를 대칭 모노이드 범주로 대체하거나 불 대수를 C*-대수로 대체하여 고전 논리의 해석을 개선하는 것으로 볼 수 있다. 고전 선형 논리 (CLL)의 언어는 BNF 표기법에 의해 귀납적으로 정의된다. 여기서 p 및 p⊥ 는 논리적 원자 범위이다. 다음 용어를 추가로 사용할 수 있다. 이항 접속사 ⊗, ⊕, & 및 ⅋는 결합 및 교환 가능한다. 1은 ⊗의 단위, 0은 ⊕의 단위, ⊥는 ⅋의 단위, ⊤는 &의 단위이다. CLL의 모든 명제 A에는 다음과 같이 정의된 A⊥가 있다. (-)⊥ 는 대합이다. 즉, 모든 명제에 대해 A⊥⊥ = A A⊥ 선형 부정이라고한다. 표의 열은 극성 이라고 하는 선형 논리의 연결자를 분류하는 또 다른 방법을 제안한다. ⊗, ⊕, 1, 0, !는 positive라고 하고, ⅋, &, ⊥, ⊤, ?는 negative라고 한다. A ⊸ B := A⊥ ⅋ B로 정의할 수 있다. La logica lineare è una proposta da come un raffinamento della logica classica ed intuizionista, coniugando le dualità che caratterizzano i connettivi della prima con le proprietà costruttive della seconda. Sebbene questo sistema logico sia un oggetto di studio fine a se stesso, più in generale le idee della logica lineare hanno influito in settori come i linguaggi di programmazione, la o la fisica dei quanti e la linguistica, in particolare per la sua enfasi sulle risorse limitate, la dualità e l'interazione. La logica lineare, di per sé, si presta a molteplici presentazioni e spiegazioni. Dal punto di vista della teoria della dimostrazione deriva da un'analisi del calcolo dei sequenti classico in cui gli usi della e di (regole strutturali) sono attentamente regolati. Al livello operativo questo significa che la deduzione logica non riguarda più solo l'espandere un insieme di "proposizioni vere", ma è anche un modo per manipolare risorse che non possono essere sempre duplicate o eliminate a piacere. In termini di semplici modelli denotazionali, la logica lineare può essere considerata come un raffinamento dell'interpretazione della logica intuizionistica sostituendo le con categorie monoidali simmetriche, o dell'interpretazione della logica classica sostituendo le algebre booleane con le . Lógica linear é um lógica subestrutural proposta por Jean-Yves Girard como um refinamento da lógica clássica e intuicionista, juntando as dualidades da primeira com muitas das propriedades construtivas da última. Embora a lógica também tenha sido estudada por si mesma, mais amplamente, as ideias da lógica linear têm influenciado em campos como linguagens de programação, jogos de semântica e física quântica, bem como a linguística, particularmente devido a sua ênfase na limitação de recursos, dualidade e interação. A lógica linear presta-se a muitas apresentações, explicações e intuições diferentes. A prova-teoricamente, deriva de uma análise de cálculo sequencial clássico em que os usos das regras estruturais de contração e enfraquecimento são cuidadosamente controlados. Operacionalmente, isso significa que a dedução lógica já não se limita a uma coleção cada vez maior de "verdades" persistentes, mas é, também, uma maneira de manipular recursos que nem sempre podem ser duplicados ou descartados à vontade. Em termos de modelos denotacionais simples, a lógica linear pode ser vista como refinamento da interpretação da lógica intuicionista, substituindo as categorias fechadas cartesianas por categorias monoidais simétricas, ou da interpretação da lógica clássica, substituindo as álgebras booleanas por C *-álgebras. Lineární logika je verze formální logiky, v níž při odvození dochází k vyřazení antecedentu z množiny formulí. Máme-li napříklada pravidlo (lineární implikaci),můžeme odvodit,tj. A "zmizí" a není již k dispozici pro další pravidla. Používá se zejména při zpracování přirozeného jazyka pro generování logické reprezentace vět (poprvé byla pro tuto úlohu použita v ).Například význam slovesa věty John loves Mary lze vyjádřit takto: Protože v lineaární logice platí a lineární konjunkce je komutativní, lze stejný konstruktor významu použít beze změny také například pro topikalizovanou verzi stejné věty Mary, John loves. Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics (because linear logic can be seen as the logic of quantum information theory), as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction. Linear logic lends itself to many different presentations, explanations, and intuitions.Proof-theoretically, it derives from an analysis of classical sequent calculus in which uses of (the structural rules) contraction and weakening are carefully controlled. Operationally, this means that logical deduction is no longer merely about an ever-expanding collection of persistent "truths", but also a way of manipulating resources that cannot always be duplicated or thrown away at will. In terms of simple denotational models, linear logic may be seen as refining the interpretation of intuitionistic logic by replacing cartesian (closed) categories by symmetric monoidal (closed) categories, or the interpretation of classical logic by replacing Boolean algebras by C*-algebras. En logique mathématique et plus précisément en théorie de la démonstration, la logique linéaire, inventée par le logicien Jean-Yves Girard en 1986, est un système formel qui, du point de vue logique, décompose et analyse les logiques classique et intuitionniste et, du point de vue calculatoire, est un système de type pour le lambda-calcul permettant de spécifier certains usages des ressources. La logique classique n'étudie pas les aspects les plus élémentaires du raisonnement. Sa structure peut être décomposée dans des systèmes formels plus élémentaires qui décrivent des étapes plus fines de la déduction ; en particulier, il est possible de s'intéresser à des logiques où certaines règles de la logique classique n'existent pas. De telles logiques sont appelées des logiques sous-structurelles. L'une de ces logiques sous-structurelles est la logique linéaire ; il lui manque en particulier la règle de contraction de la logique classique qui dit en gros que si on peut faire un raisonnement avec une même hypothèse invoquée deux fois, on peut faire le même raisonnement sans dupliquer cette hypothèse et la règle d'affaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement. 在数理逻辑中，线性逻辑是拒绝“弱化”和“收缩”的结构规则的一种亚结构逻辑。对此解释是“假设是资源”:在证明中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如经典逻辑或直觉逻辑，那里统治判断是“真理”，它可以按需要被自由的使用多次。例如，从命题A和A ⇒ B能按如下步骤得出结果A ∧ B: 1. * （1）在假定A和A ⇒ B上应用肯定前件（或蕴涵除去）得到结论B。 2. * （2）A和（1）的合取的得到结论A ∧ B。 这经常被符号化表示为相继式：A, A ⇒ B B。在上述证明中"消费"了A为真的事实；这种真理的"自由"通常是在形式化数学中所需要的。 但是，真理经常在应用于关于这个世界的陈述的时候太抽象或不实用。比如，假设我有一夸脱的牛奶，我能用它制作一磅奶酪。如果我决定把我的所有牛奶都制成奶酪，我就不能下结论说我有牛奶和奶酪二者! 上面的逻辑模式让我们得到结论：牛奶, 牛奶⇒奶酪牛奶∧奶酪（这里的牛奶表示命题"我有一夸脱牛奶"，等等）。普通逻辑建模这个活动失败是由于牛奶、奶酪一般是资源：资源的数量不像真理是可以随意使用和支配的自由事实，而是必须在所有"状态变更"中仔细计量的。关于牛奶制奶酪活动的准确陈述是： 从一夸脱牛奶和从一夸脱牛奶转换出一磅奶酪的过程，我们获得一磅奶酪。 在线性逻辑中我们写为：牛奶, 牛奶奶酪奶酪，使用了不同的连结词（替代了⇒）和不同的逻辑蕴涵符号。 线性逻辑由法国数学家让·伊夫·吉拉德（Jean-Yves Girard）在1987年提出。 Линейная логика (англ. Linear Logic — это подструктурная логика, предложенная (англ. Jean-Yves Girard) как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней, введена и используется для логических рассуждений, учитывающих расход некоторого ресурса. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации), лингвистика.
gold:hypernym
dbr:Logic
prov:wasDerivedFrom
wikipedia-en:Linear_logic?oldid=1115771213&ns=0
dbo:wikiPageLength
32710
foaf:isPrimaryTopicOf
wikipedia-en:Linear_logic