Linear logic (original) (raw)
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
| Property | Value |
|---|---|
| dbo:abstract | 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. (cs) 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 (es) 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) 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. (fr) 선형 논리(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로 정의할 수 있다. (ko) 線形論理（せんけいろんり、英: 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年、フランスの論理学者ジャン＝イヴ・ジラールが提唱した。 (ja) 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 . (it) 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. (pt) Линейная логика (англ. Linear Logic — это подструктурная логика, предложенная (англ. Jean-Yves Girard) как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней, введена и используется для логических рассуждений, учитывающих расход некоторого ресурса. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации), лингвистика. (ru) 在数理逻辑中，线性逻辑是拒绝“弱化”和“收缩”的结构规则的一种亚结构逻辑。对此解释是“假设是资源”:在证明中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如经典逻辑或直觉逻辑，那里统治判断是“真理”，它可以按需要被自由的使用多次。例如，从命题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年提出。 (zh) |
| dbo:wikiPageExternalLink | http://bach.istc.kobe-u.ac.jp/llprover/ http://llwiki.ens-lyon.fr/ http://www.dicosmo.org/CourseNotes/LinLog/ http://www.brics.dk/LS/96/6/BRICS-LS-96-6.pdf http://girard.perso.math.cnrs.fr/linear.pdf http://www.csl.sri.com/users/lincoln/ http://www.csl.sri.com/~lincoln/papers/sigact92.ps https://web.archive.org/web/20060925141642/http:/www.pps.jussieu.fr/~dicosmo/index.html.en https://web.archive.org/web/20160704202340/http:/www.cs.man.ac.uk/~pt/stable/Proofs+Types.html http://plato.stanford.edu/entries/logic-linear/ http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html http://www.lix.polytechnique.fr/Labo/Dale.Miller/ http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/llp.pdf |
| dbo:wikiPageID | 579675 (xsd:integer) |
| dbo:wikiPageLength | 32710 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1115771213 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Programming_languages dbr:Proof_net dbr:Quantum_information_theory dbc:Linear_logic dbr:Monotonicity_of_entailment dbr:Boolean_algebras dbr:Denotational_semantics dbc:Logic dbr:Cut-elimination_theorem dbr:C*-algebras dbr:De_Morgan's_laws dbr:EXPSPACE dbr:Intuitionistic_logic dbr:PSPACE-complete dbr:Substructural_type_system dbr:Quantum_physics dbr:Analytic_proof dbr:Geometry_of_interaction dbr:Noncommutative_logic dbr:Structural_rule dbr:NP-complete dbr:Symmetric_monoidal_categories dbr:Linear_type_system dbr:Logical_conjunction dbr:Ludics dbr:Completeness_of_atomic_initial_sequents dbr:Computability_logic dbr:Idempotency_of_entailment dbr:Identity_element dbr:Theoretical_Computer_Science_(journal) dbr:Backus–Naur_form dbr:Admissible_rule dbr:Tony_Hoare dbr:Game_semantics dbr:Linguistics dbr:Logical_harmony dbr:Logical_truth dbr:Lollipop dbr:Duality_(mathematics) dbc:Non-classical_logic dbr:First-order_logic dbr:Chu_space dbr:Frame_problem dbr:Entailment dbr:Logical_connective dbr:Logical_consequence dbr:Logical_disjunction dbr:Proof_theory dbr:Atomic_formula dbr:Involution_(mathematics) dbr:Jean-Yves_Girard dbr:Affine_logic dbc:Substructural_logic dbr:Higher-order_logic dbr:Classical_logic dbr:Constructivism_(mathematics) dbr:Canonical_form dbr:Sequent_calculus dbr:Turnstile_(symbol) dbr:Undecidable_problem dbr:Strict_logic dbr:Normal_modal_logic dbr:Uniqueness_type dbr:Substructural_logic dbr:Linear_logic_programming dbr:Petri_nets dbr:Cartesian_closed_categories dbr:Lambda-calculus dbr:Relevant_logic dbr:A._S._Troelstra dbr:Gödel–Gentzen_negative_translation dbr:Exchange_rule dbr:Horn_clauses dbr:Logic_of_unity |
| dbp:date | May 2015 (en) |
| dbp:reason | It is difficult to guess what this might mean without a link (en) |
| dbp:wikiPageUsesTemplate | dbt:= dbt:Citation_needed dbt:Clarify dbt:Commons_category-inline dbt:Main dbt:Math dbt:Portal dbt:Redirect dbt:Reflist dbt:See_also dbt:Short_description dbt:Isbn dbt:Tee dbt:Non-classical_logic |
| dcterms:subject | dbc:Linear_logic dbc:Logic dbc:Non-classical_logic dbc:Substructural_logic |
| gold:hypernym | dbr:Logic |
| rdf:type | owl:Thing |
| rdfs:comment | 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 (es) Линейная логика (англ. Linear Logic — это подструктурная логика, предложенная (англ. Jean-Yves Girard) как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней, введена и используется для логических рассуждений, учитывающих расход некоторого ресурса. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации), лингвистика. (ru) 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: (cs) 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. (en) 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. (fr) 線形論理（せんけいろんり、英: 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 が真であるという事実を「消費」している。この真理の「気軽さ」は形式手法では一般に必須である。 このような活動を通常の論理でうまく表せないのは、クリームやバターなどの「資源」全般の性質によるものである。ある量の資源は、真理のように好きなように使ったり始末したりできず、全ての「状態変化」について注意深く見ていかなければならない。バター作りを正確に表すと、次のようになる。 (ja) 선형 논리(Linear logic)는 장-이브 지라르(Jean-Yves Girard)가 고전 및 직관 논리의 개선으로 제안한 하위 구조 논리로 전자의 쌍대성을 후자의 구성주의적 속성과 결합한다. 논리학도 그 자체로 연구되었지만, 보다 넓게는 선형 논리학의 아이디어가 프로그래밍 언어, 게임 의미론, 양자 물리학, 언어학 같은 분야에 영향을 미쳤다. (선형 논리는 양자 정보 이론 의 논리라고 볼 수 있기 때문이다.) 선형 논리는 다양한 프레젠테이션, 설명 및 직관에 적합하다. 증명 이론상, 그것은 시퀀트 계산의 분석에서 파생된다. 이것은 논리적 추론이 더 이상 계속해서 확장되는 지속적인 "진리"의 모음에 관한 것이 아니라, 마음대로 복제하거나 버릴 수 없는 자원을 조작하는 방법이라는 것을 의미한다. 단순 표시적 의미론 관점에서 선형 논리는 데카르트 닫힌 범주를 대칭 모노이드 범주로 대체하거나 불 대수를 C*-대수로 대체하여 고전 논리의 해석을 개선하는 것으로 볼 수 있다. 고전 선형 논리 (CLL)의 언어는 BNF 표기법에 의해 귀납적으로 정의된다. 여기서 p 및 p⊥ 는 논리적 원자 범위이다. 다음 용어를 추가로 사용할 수 있다. (ko) 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. (it) 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. (pt) 在数理逻辑中，线性逻辑是拒绝“弱化”和“收缩”的结构规则的一种亚结构逻辑。对此解释是“假设是资源”:在证明中所有假设必须被消费“精确一次”。这区别于平常的逻辑比如经典逻辑或直觉逻辑，那里统治判断是“真理”，它可以按需要被自由的使用多次。例如，从命题A和A ⇒ B能按如下步骤得出结果A ∧ B: 1. * （1）在假定A和A ⇒ B上应用肯定前件（或蕴涵除去）得到结论B。 2. * （2）A和（1）的合取的得到结论A ∧ B。 这经常被符号化表示为相继式：A, A ⇒ B B。在上述证明中"消费"了A为真的事实；这种真理的"自由"通常是在形式化数学中所需要的。 但是，真理经常在应用于关于这个世界的陈述的时候太抽象或不实用。比如，假设我有一夸脱的牛奶，我能用它制作一磅奶酪。如果我决定把我的所有牛奶都制成奶酪，我就不能下结论说我有牛奶和奶酪二者! 上面的逻辑模式让我们得到结论：牛奶, 牛奶⇒奶酪牛奶∧奶酪（这里的牛奶表示命题"我有一夸脱牛奶"，等等）。普通逻辑建模这个活动失败是由于牛奶、奶酪一般是资源：资源的数量不像真理是可以随意使用和支配的自由事实，而是必须在所有"状态变更"中仔细计量的。关于牛奶制奶酪活动的准确陈述是： 从一夸脱牛奶和从一夸脱牛奶转换出一磅奶酪的过程，我们获得一磅奶酪。 在线性逻辑中我们写为：牛奶, 牛奶奶酪奶酪，使用了不同的连结词（替代了⇒）和不同的逻辑蕴涵符号。 (zh) |
| rdfs:label | Linear logic (en) Lineární logika (cs) Lógica lineal (es) Logica lineare (it) Logique linéaire (fr) 선형 논리 (ko) 線形論理 (ja) Lógica linear (pt) Линейная логика (ru) 线性逻辑 (zh) |
| rdfs:seeAlso | dbr:Quantale |
| owl:sameAs | freebase:Linear logic wikidata:Linear logic dbpedia-cs:Linear logic dbpedia-es:Linear logic dbpedia-fr:Linear logic dbpedia-it:Linear logic dbpedia-ja:Linear logic dbpedia-ko:Linear logic dbpedia-pt:Linear logic dbpedia-ru:Linear logic dbpedia-zh:Linear logic https://global.dbpedia.org/id/4zVHe |
| prov:wasDerivedFrom | wikipedia-en:Linear_logic?oldid=1115771213&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Linear_logic |
| is dbo:knownFor of | dbr:Jean-Yves_Girard |
| is dbo:wikiPageRedirects of | dbr:⊸ dbr:Linear_Logic dbr:⅋ dbr:Intuitionistic_linear_logic dbr:Linear_L |
| is dbo:wikiPageWikiLink of | dbr:Prolog dbr:Proof_net dbr:Quantum_logic dbr:Question_mark dbr:Question_mark_(disambiguation) dbr:List_of_XML_and_HTML_character_entity_references dbr:List_of_functional_programming_topics dbr:Monoidal_category dbr:Monotonicity_of_entailment dbr:Denotational_semantics dbr:Algebra_of_sets dbr:List_of_important_publications_in_theoretical_computer_science dbr:Currying dbr:Decidability_(logic) dbr:⊸ dbr:Deviant_logic dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(I–Q) dbr:Intellect dbr:Interaction_nets dbr:Intuitionistic_logic dbr:Ivan_Orlov_(philosopher) dbr:List_of_mathematical_logic_topics dbr:List_of_rules_of_inference dbr:Substructural_type_system dbr:String_diagram dbr:Timeline_of_category_theory_and_related_mathematics dbr:*-autonomous_category dbr:Geometry_of_interaction dbr:Noncommutative_logic dbr:Quantum_programming dbr:François_Fages dbr:Braided_monoidal_category dbr:Concatenative_programming_language dbr:Andreas_Blass dbr:Anne_Sjerp_Troelstra dbr:Ludics dbr:Calculus_of_structures dbr:Closed_monoidal_category dbr:Computability_logic dbr:Idempotency_of_entailment dbr:Autonomous_category dbr:Type_system dbr:Game_semantics dbr:Giorgi_Japaridze dbr:Logic_programming dbr:Logics_for_computability dbr:Paraconsistent_logic dbr:No-cloning_theorem dbr:No-deleting_theorem dbr:Actor_model dbr:Curry–Howard_correspondence dbr:Exclamation_mark dbr:Chu_space dbr:Dialectica_interpretation dbr:Dialectica_space dbr:Dialogical_logic dbr:Focused_proof dbr:Frame_problem dbr:Glue_semantics dbr:List_of_French_inventions_and_discoveries dbr:Natural_deduction dbr:Proof_theory dbr:Henry_Baker_(computer_scientist) dbr:Jean-Yves_Girard dbr:Łukasiewicz_logic dbr:Absorption_law dbr:Affine_logic dbr:Coherent_space dbr:Why_Not dbr:Bunched_logic dbr:Cirquent_calculus dbr:Free_choice_inference dbr:Categorial_grammar dbr:Lollipop_(disambiguation) dbr:Proof_mining dbr:Linear_Logic dbr:Residuated_lattice dbr:Valeria_de_Paiva dbr:Non-classical_logic dbr:Patrick_Lincoln dbr:Outline_of_logic dbr:Outline_of_philosophy dbr:⅋ dbr:Uniqueness_type dbr:Substructural_logic dbr:Intuitionistic_linear_logic dbr:Linear_L |
| is dbp:knownFor of | dbr:Jean-Yves_Girard |
| is foaf:primaryTopic of | wikipedia-en:Linear_logic |