{"entities":{"Q534705":{"pageid":536472,"ns":120,"title":"Item:Q534705","lastrevid":62615718,"modified":"2026-04-11T07:17:54Z","type":"item","id":"Q534705","labels":{"en":{"language":"en","value":"A linear algorithm for MLL proof net correctness and sequentialization"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5886383"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$73792ABF-4A76-4E4F-9277-87D37680BAC1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fa05735a38684fd4082ff8b47224b6a5d9036341","datavalue":{"value":{"text":"A linear algorithm for MLL proof net correctness and sequentialization","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q534705$6F6BAD19-35E1-4D68-9F0F-1F56D6FA5947","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c7f8d5a8f552d327d162666d5e845670ad43e435","datavalue":{"value":"1222.03067","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q534705$5876C519-6998-4BF4-A728-990F676021F0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"54493f09366d013460fab20d41ad3e9ee49fb384","datavalue":{"value":{"entity-type":"item","numeric-id":534704,"id":"Q534704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$4C406F07-905A-4E3C-8BA2-15B7557F5A19","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$B7DC42BC-FDDB-4ACF-B5FB-43734BDABE9E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6355dd651d7e8925edcf5ba080dbea252734508c","datavalue":{"value":{"time":"+2011-05-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q534705$AEB8F834-2A8E-4E65-A234-094690771F05","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"bf7c634f29b6d13c7d81dccff849247a8eb94124","datavalue":{"value":"The paper presents in full detail a linear algorithm for verifying the correctness of proof nets for multiplicative linear logic without units. It extends a previous paper of the same author [\\textit{S. Guerrini}, ``Correctness of multiplicative proof nets is linear'', in: 14th symposium on logic in computer science, Trento, 1999. Los Alamitos, CA: IEEE Computer Society Press. 454--463 (1999)], where the linear algorithm (a pioneer in the literature on implementing a correctness criterion for multiplicative proof structures in linear time) was first introduced. The algorithm, which is linear when executed on sequential RAMs, is essentially a reformulation of Danos' contractibility criterion in terms of a sort of unification [\\textit{V. Danos}, Une application de la logique lin\u00e9aire \u00e0 l'\u00e9tude des processus de normalisation (principalement du lambda-calcul). Ph.D. Thesis, Universit\u00e9 Paris 1 (1990); \\textit{S. Guerrini} and \\textit{A. Masini}, Theor. Comput. Sci. 254, No. 1--2, 317--335 (2001; Zbl 0974.68077); \\textit{Y. Lafont}, Lond. Math. Soc. Lect. Note Ser. 222, 225--247 (1995; Zbl 0830.03028)]. A direct implementation of the unification criterion, which can be formulated as a disjoint-set union-find problem, leads to a quasi-linear algorithm. The solution results essentially from an efficient implementation of parsing as a sort of unification. Linearity was achieved after observing that the disjoint-set union-find at the basis of the unification criterion is a special case of union-find with a real linear-time solution. For related work in the area see [\\textit{A. S. Murawski} and \\textit{C.-H. L. Ong}, ``Dominator trees and fast verification of proof nets'', in: 15th annual IEEE symposium on logic in computer science, Santa Barbara, CA, 2000. Los Alamitos, CA: IEEE Computer Society Press. 181--191 (2000); \\textit{A. S. Murawski} and \\textit{C.-H. L. Ong}, ``Fast verification of MLL proof nets via IMLL'', ACM Trans. Comput. Log. 7, No. 3, 473--498 (2006)].","type":"string"},"datatype":"string"},"type":"statement","id":"Q534705$3E71C2AD-E221-488B-BD36-A409672E84D0","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"15a5be954de63b9a09120e92802adc210813c3df","datavalue":{"value":{"entity-type":"item","numeric-id":424544,"id":"Q424544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$366F5F91-2088-45B4-AA60-A45B3FA33BB2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q534705$D8D94646-DA4F-4626-8E4F-4C12EBE6CF59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q534705$34343BE0-5780-4C59-BF66-4D521F2882C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q534705$8F52B09E-296B-4D5E-B8A3-A09492967171","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"db8633a74f5e2d654eca3517362014fbb86568cb","datavalue":{"value":"5886383","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q534705$E01C70C8-1574-4C6E-BDE3-D5A76E6F532A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ef07b3138676aab0c29826b8e961bd9e50153980","datavalue":{"value":"multiplicative linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q534705$C4A6B824-7A33-4653-B80F-56B678ABFD2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d82d54321dd9799ec54c6e2eeabcd189cda5e80a","datavalue":{"value":"proof nets","type":"string"},"datatype":"string"},"type":"statement","id":"Q534705$8A20789E-1687-40EB-8F8B-57FEF8DDCEE3","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$5CB057B9-867A-4951-A4DB-799D22C62DED","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f6b76817a6b3fcf7d0cc6ce4800b71a4bd6e0e66","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2010.12.021","type":"string"},"datatype":"url"},"type":"statement","id":"Q534705$4966D67D-94E6-4EAB-AC68-F4CF493C3F81","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e2ed0c851c113b6e42aba3a6ed8d746abccdb1da","datavalue":{"value":"W2011228482","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q534705$D8D3342F-8D91-4565-9334-AF423C1D4AB2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea08311e5cede8e103fdccb0049502f7fb72a285","datavalue":{"value":{"entity-type":"item","numeric-id":1264140,"id":"Q1264140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$21E1C3FF-094F-4683-B7A0-DB9DC8A0A176","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17b46f23e1d95210ec444c78dd7a8edd18f2e48d","datavalue":{"value":{"entity-type":"item","numeric-id":1062461,"id":"Q1062461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$0C90765C-A111-434D-85D2-8DBA9CF894EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a2b2a8cf71a298beb3d5742fd0312db85012cf7","datavalue":{"value":{"entity-type":"item","numeric-id":579249,"id":"Q579249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$1E31A738-2190-45EF-BB45-70B539194DEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d2e18d1df9fdf7c997855f23fd7e29219c01e7f","datavalue":{"value":{"entity-type":"item","numeric-id":5940925,"id":"Q5940925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$F05606A1-F357-4D4A-B0C4-2A82E24381EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"157bc9663d30f618111621fe105686ca18dcc366","datavalue":{"value":{"entity-type":"item","numeric-id":3608429,"id":"Q3608429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$14B4B229-669D-4C64-9E56-A5F83DB982AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a48c61c6138784426830f34f60c6e6c51b112861","datavalue":{"value":{"entity-type":"item","numeric-id":4842976,"id":"Q4842976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$8A513754-CFAC-4B29-BACD-36202EE00579","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c9465d6417bb77bd19e652eaf6c381784d12e8b","datavalue":{"value":{"entity-type":"item","numeric-id":3936229,"id":"Q3936229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$CCB9FE04-B648-4D7E-9B47-386C92E37E2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b546780d40c50376f423802c49749e1215bdce97","datavalue":{"value":{"entity-type":"item","numeric-id":5277754,"id":"Q5277754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$C9327E55-5A96-45DD-B827-5173AC8ACDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b25a1f1869b4bd8cc44b5d75a6f4485919d4ebdd","datavalue":{"value":{"entity-type":"item","numeric-id":4328819,"id":"Q4328819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$CEF60DD6-B1DD-4272-8793-A9ECEA6EA0E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"932383d1ac997ed208ef47dcb574b592efaf75b3","datavalue":{"value":{"entity-type":"item","numeric-id":4065031,"id":"Q4065031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q534705$9B837719-73FC-4CE1-8A62-E35A1447EEA2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e31d3a277780c6a929b4f0ce7de323b1c830aa12","datavalue":{"value":"10.1016/J.TCS.2010.12.021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q534705$64E56273-848A-426E-9D6A-3231AF278981","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01198edb11dec49297fe8545b7c5cae69736ac2c","datavalue":{"value":{"entity-type":"item","numeric-id":5277754,"id":"Q5277754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a735722258ad7560140f252a047528e9a86a9d05","datavalue":{"value":{"amount":"+0.8554108738899231","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q534705$2E2B9CC1-469E-4AA9-8A03-9D8EE03D228F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18cfa5a292c05ae87a6d6dcbdb2ae28a02d2c098","datavalue":{"value":{"entity-type":"item","numeric-id":4328819,"id":"Q4328819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed2cf1d11de6a4aedeb6a4beab9aa7949baaa478","datavalue":{"value":{"amount":"+0.8307124376296997","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q534705$BECF60A7-7987-4D31-80FE-736F9B226B16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3fd19c9ec9c20debb1519572d873334eeb991120","datavalue":{"value":{"entity-type":"item","numeric-id":1892938,"id":"Q1892938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed2cf1d11de6a4aedeb6a4beab9aa7949baaa478","datavalue":{"value":{"amount":"+0.8307124376296997","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q534705$87D6DB91-0239-4713-B980-63CCE9C07C37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"debd68b9486f4064fa537e8ed50615f4b651750c","datavalue":{"value":{"entity-type":"item","numeric-id":4217606,"id":"Q4217606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46934890775e09a1f2959ffd0d4ea648fa80b074","datavalue":{"value":{"amount":"+0.8174916505813599","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q534705$55576BE5-CE29-4C96-9F68-A20972558529","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97c296e284c341a787d02fb7456570fa19e43dc6","datavalue":{"value":{"entity-type":"item","numeric-id":3608429,"id":"Q3608429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c931ea862af26b01e3029c9883282ac91c7db62","datavalue":{"value":{"amount":"+0.8166161179542542","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q534705$812F5248-4EC8-43C0-9297-57F1B22A6724","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A linear algorithm for MLL proof net correctness and sequentialization","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_linear_algorithm_for_MLL_proof_net_correctness_and_sequentialization"}}}}}