{"entities":{"Q1340963":{"pageid":1351702,"ns":120,"title":"Item:Q1340963","lastrevid":68506644,"modified":"2026-04-13T00:10:11Z","type":"item","id":"Q1340963","labels":{"en":{"language":"en","value":"Proof strategies in linear logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 704957"}},"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":"Q1340963$E9368E86-3309-4CEC-BCD2-B9D211F5FF86","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f83a30a4636426a6638c24f8ae3acff5a6b1c248","datavalue":{"value":{"text":"Proof strategies in linear logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1340963$FAB1A582-B69E-405D-A0C1-D99AD219326E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"90c75ef1caba7adf42c26f46d731ded152e721f3","datavalue":{"value":"0821.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340963$9EEACB20-A9AD-47F1-99AC-075F0BB96A38","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"29d8e373e8eb0061cb0d93fcb89f2486689c8320","datavalue":{"value":"10.1007/BF00885763","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340963$0127E120-3621-4F21-B2E4-38245D75BF67","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"50dfba14eecf8f7e9f64ea004fb9b72dca6eb33f","datavalue":{"value":{"entity-type":"item","numeric-id":1181716,"id":"Q1181716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$D99EDBF3-D22A-48CE-BF39-6783AD1D3028","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$BA3B1C7C-8546-4C8D-9921-C2581B9FB493","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"89a5af496da52109cb9fd8ee43aa6e112a9ba241","datavalue":{"value":{"time":"+1994-12-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1340963$299234B7-19B0-4B00-83E5-05F2338BF9EF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c859bdac7f41e0b790d50425938032eccc4501ab","datavalue":{"value":"Contraction and weakening are deduction rules that allow to use a hypothesis several times, once or never in a proof. Dealing with such rules is a major problem in automated theorem proving. Without these rules predicate calculus is decidable and simple algorithms can be designed.    Linear logic is a refinement of classical logic that allows some control on contraction and weakening. Wide fragments of linear logic are decidable and their investigation has been recently a rather active field of research.    In this paper, the author investigates and compares several proof search methods (bottom-up and top-down) for propositional and predicate linear logic. One of the issues of the paper is to get decision methods for some fragments of linear logic (e.g., without exponentials) but also to implement algorithms as efficient as possible: performances of the algorithms (in terms of time of execution and number of propositions generated) are analyzed on many examples and several optimizations of the naive algorithms are proposed.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340963$F9FC8234-EF13-422B-9188-E6A0EA56788B","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"085e1d1d24be02ea23effd8a6c73fa275fc02f04","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$5A389960-4697-4725-BF06-ED8B8699D57F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340963$28F505AF-7AC0-4C43-9899-43F5E160D5F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340963$33EB0396-E168-4A96-9C5D-2EA5B5DA0C65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340963$36CF6D87-D561-421F-BAAA-A66ECC24728F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eb7dfe0b6dba2bd1a72ca7fea0d81bbbe97ec30f","datavalue":{"value":"704957","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340963$E7B9EA51-C2FC-4B8F-9E19-A77EEE25D9C5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1c9977afeaac4d053aef4e5b5c50df2441a2faf8","datavalue":{"value":"resolution method","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340963$A8B23E12-AA76-47DC-95D0-542070A03E8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5253d57585b205f2e450b1a6d5d3fabd58efc18e","datavalue":{"value":"decision methods for fragments of linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340963$FFF04AE1-32BD-48AC-849A-00D341EEBDF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340963$AD07E878-F0F2-47B6-B3D9-DA53A7025AD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fef5cfaefae7240b857076a2c6c12c59644fa0a0","datavalue":{"value":"proof search methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340963$D7530C38-0AD6-4546-A0DF-E00C77F8B06D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340963$03E90BB2-7C17-4970-BB45-A62394BF00E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d607627523840bd0bf4407097f29a3a99ef4a0a8","datavalue":{"value":"algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q1340963$C135FB9D-99A9-4C82-8289-E75F149E0367","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9bea83566ad047ec39e22bd8867e363c00af7d87","datavalue":{"value":{"entity-type":"item","numeric-id":5975143,"id":"Q5975143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$AB4F604B-DD7A-4422-95CF-E42B61BCD5F0","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":"Q1340963$F9DA3369-32F8-4337-9EAA-088A4FDDFAE5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"42bdbea0160e788f4fb95a24a8a29ffb0eadc069","datavalue":{"value":{"entity-type":"item","numeric-id":4018167,"id":"Q4018167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$7F1087E2-70A3-49A6-911A-6232F43D80FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff150f7d1a7818365b378c3430ce3254cb0dd643","datavalue":{"value":{"entity-type":"item","numeric-id":2757832,"id":"Q2757832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$3BC36FDC-F9D0-4ACC-93A5-EB0856BB2913","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":"Q1340963$901C9C57-9568-43C5-A153-5CBBF38A9BF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b537ca273e85bc385c65ddbbf65cb49fb61377fc","datavalue":{"value":{"entity-type":"item","numeric-id":4255503,"id":"Q4255503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$331B8B75-30EB-4DB6-B180-FA94C7F28D97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"483505c109466864c272a9800591d657b7054034","datavalue":{"value":{"entity-type":"item","numeric-id":1327384,"id":"Q1327384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$1345C18B-1C64-45C7-91A2-32D94628CC9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c6d07dd80de4de8f6f1d51aa5d78e790a6fd51","datavalue":{"value":{"entity-type":"item","numeric-id":5812175,"id":"Q5812175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$EC783F22-9D25-4E38-AFE4-DD7D5E43D7CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"074134d8b33bdd9cca293a6e8f5f8ee888ec9918","datavalue":{"value":{"entity-type":"item","numeric-id":1192352,"id":"Q1192352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$632216DA-9748-4EF9-B7A7-C4609B7588B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ceaa83d5b438e37e6fe3f36e90e82ef20643e21d","datavalue":{"value":{"entity-type":"item","numeric-id":4202932,"id":"Q4202932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$DF4F55DC-F60A-48B3-B060-8145DC676A6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9e2984aad27cb3e25159a04dea706a44d204c70","datavalue":{"value":{"entity-type":"item","numeric-id":4766612,"id":"Q4766612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$EC1DAB37-AB5D-4E5A-B2A3-672207AB0A6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"164d5958e5083b10f8e82ed42140727a0ef780a4","datavalue":{"value":{"entity-type":"item","numeric-id":3972527,"id":"Q3972527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$FAD44D71-BEE4-4861-A031-57C9CAC60B68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de94d8f291c9390ca640108081f24e51c850678c","datavalue":{"value":{"entity-type":"item","numeric-id":1314284,"id":"Q1314284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$07145034-91F1-4DE5-9839-4EFFE516462E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1340963$EF27B242-E834-4BB9-9659-989194696220","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0ec9ed95782ddb842191437fd7c41895cda41f82","datavalue":{"value":"https://doi.org/10.1007/bf00885763","type":"string"},"datatype":"url"},"type":"statement","id":"Q1340963$7E4344D5-EB7B-4FAF-8FA1-B4CECC5586F2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"75eaf8e31cedffe2d5b519a4919f58b59d727e6e","datavalue":{"value":"W71891286","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1340963$662E7334-F732-481A-B122-E29B8EC9E687","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f60160024512c73f3c431b760ec9d2b4a9aa14ec","datavalue":{"value":{"entity-type":"item","numeric-id":1342248,"id":"Q1342248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0af58384cf66f23ad6992b2b0b2f5b7ec53a01a","datavalue":{"value":{"amount":"+0.8136394023895264","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":"Q1340963$CA05D26C-FBF9-42AE-8B62-E362C0676737","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d97ce14ea95f4a3fc8c3af98620ebc361d7a77fb","datavalue":{"value":{"entity-type":"item","numeric-id":1192352,"id":"Q1192352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0af58384cf66f23ad6992b2b0b2f5b7ec53a01a","datavalue":{"value":{"amount":"+0.8136394023895264","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":"Q1340963$B41A6753-854F-4F26-920B-E7EBB0A3CDA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"181c7c870ef6785e31b0e6508f57bb8f8d4d6d91","datavalue":{"value":{"entity-type":"item","numeric-id":4501142,"id":"Q4501142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6ab97dde4aa9171e3e940c1c75baa22afd3bfbb","datavalue":{"value":{"amount":"+0.792586624622345","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":"Q1340963$B89AEEA7-E71C-4A14-AE3F-FD661E58909C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"524ab2973279b77374bf2818b4cbe86ddc56c2d8","datavalue":{"value":{"entity-type":"item","numeric-id":2757832,"id":"Q2757832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37af0d0daee338fe32cf3eb7f6aa513ada2a21fc","datavalue":{"value":{"amount":"+0.7860214114189148","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":"Q1340963$9DF49E5B-EF33-415D-8EB7-C6BA2962D78D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66b92e0c5e37d8649b02e898e82086aff0c3e28a","datavalue":{"value":{"entity-type":"item","numeric-id":4222837,"id":"Q4222837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e2ebda0079c5e3c625ff2833aebe58078e4484f","datavalue":{"value":{"amount":"+0.7709494233131409","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":"Q1340963$78B725F0-5EB4-4A1A-A6FC-D6CC04497F54","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof strategies in linear logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_strategies_in_linear_logic"}}}}}