{"entities":{"Q1073009":{"pageid":1083761,"ns":120,"title":"Item:Q1073009","lastrevid":69570870,"modified":"2026-04-13T07:54:59Z","type":"item","id":"Q1073009","labels":{"en":{"language":"en","value":"A note on Presburger arithmetic with array segments, permutation and equality"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3943778"}},"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":"Q1073009$363FB4D2-32BD-4083-8D2B-0C2982AE9C82","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a22ce2d4ee0e39f5e5151e60db7ff2d6b7ec97de","datavalue":{"value":{"text":"A note on Presburger arithmetic with array segments, permutation and equality","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1073009$56D86094-E3B1-4EA6-BAF5-9C2874952596","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dc8977e93917c48b671fdaf86474b01d978361e1","datavalue":{"value":"0588.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1073009$39240BB8-AC04-42D9-BDBC-D9618A1ED2BA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e788ce81a031086705a2a256eb1274187186b9f3","datavalue":{"value":"10.1016/0020-0190(86)90039-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1073009$C30A42D8-C25E-4F07-9053-FE19C089DA27","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0fbe9a2f35bfbb97131fdd4f5f88a8af0c602f0","datavalue":{"value":{"entity-type":"item","numeric-id":688713,"id":"Q688713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1073009$44AEFBE7-4486-41CB-8E66-2645C0675D2E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1073009$AC00ADBA-9CDA-40AD-A88D-ABF09545C5C1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"63df7153432d81fa42019fcabb076c89649b0b5b","datavalue":{"value":{"time":"+1986-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1073009$B6C7C75C-4495-41D9-B4B2-1D0B32D50267","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"103d43f77fb50a13b3dd8f36340a94edc8a9c663","datavalue":{"value":"In this paper, we examine the validity (satisfiability) problem for a language containing Presburger arithmetic, finite length array segments and some fixed second order predicates. In particular, we consider the predicates: PERM, which is used to assert that two array segments contain the same multiset of elements, and \\(=\\) (equality), which is used to assert that two array segments are identical (i.e., contain the same sequence of elements and have equivalent upper and lower array bounds). It is known that the afore-mentioned (unquantified) language has a decidable validity problem. (In fact, the satisfiability problem is NP- complete.) We consider the case when equality is defined in a seemingly weaker fashion. Let \\(Y\\simeq B\\) be true if and only if array segments A and B contain the same sequence of elements. This definition of equality is more useful in the verification conditions of programs that manipulate queues and/or strings. However, we show that when this form of equality replaces the earlier variety in the previously mentioned language, the validity problem becomes undecidable.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1073009$78993643-A295-463D-8B70-7DD5852D5E67","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1073009$9A9344F0-EDC6-4F45-ABCA-E52511692BF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1073009$609250BA-6993-4EDE-BF3A-381CA05C525A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"14e68a4e76dd0c31bf9df806d123bc24127a28ce","datavalue":{"value":"3943778","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1073009$77E672D5-5D45-49B8-9610-F128C7DC8FE3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"faefc6ddeea60541290844103179759633366d75","datavalue":{"value":"second order predicates","type":"string"},"datatype":"string"},"type":"statement","id":"Q1073009$EB535115-6B6E-4275-8C9C-55815710C064","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c96c670cb5bb3f93d571a5f56f1e88c84388368c","datavalue":{"value":"validity problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1073009$18553881-9A89-4B7D-9FE5-7DF3772AEA7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0b4d6e6089943a261128dec792d30fd4cdc9763","datavalue":{"value":"satisfiability problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1073009$06A57DC8-2992-4CE5-BD96-FD037308C880","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":"Q1073009$9654683A-A158-40DB-BB14-E09B9DA88107","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"98c9dcc44a674e15827f0e22fa33f615b30c1825","datavalue":{"value":"https://doi.org/10.1016/0020-0190(86)90039-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q1073009$847A1C8B-AFD1-4125-AFAC-441B2EEB73CA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5ef653dcb7761169161b949a3bd4ec24282d65d2","datavalue":{"value":"W2059490901","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1073009$08A3EDBD-F391-46AB-BAFD-3BC89961BD61","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1073009$7473B76B-EE0B-4FA9-950A-330A90DECA0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"edcdac11d5b28d0fae3e735a21092bef44a76237","datavalue":{"value":{"entity-type":"item","numeric-id":1159191,"id":"Q1159191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1073009$EB354891-9E86-4016-8CE6-CA3CF4F87948","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"267d2692778560c926fa1a0840789871f1edb87f","datavalue":{"value":{"entity-type":"item","numeric-id":3916002,"id":"Q3916002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1073009$9A644568-D214-47CA-A440-D5C3F291EB1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c059d1355bcb0df592c7e924663d48f24f3b387e","datavalue":{"value":{"entity-type":"item","numeric-id":5613949,"id":"Q5613949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1073009$79C58E76-E10C-4AE5-AFDA-4AE7403D9AEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"393ecae0dc74f488cdf64d27da9a36da7f60c999","datavalue":{"value":{"entity-type":"item","numeric-id":4176940,"id":"Q4176940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1073009$1D59BA63-9921-43AC-943B-C5AA6FE34682","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19bb2a60e9f6ffe181fe7ecda3a8c91cb637b1a9","datavalue":{"value":{"entity-type":"item","numeric-id":3867162,"id":"Q3867162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1073009$E9B00555-0C2A-4EF3-8B16-A24B48A323EE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c6f3d173551e58c67ddcbbf85702c07b10b27a3","datavalue":{"value":{"entity-type":"item","numeric-id":4931288,"id":"Q4931288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9ec1a0d472599446683f297d27ea3b7d5a604d3","datavalue":{"value":{"amount":"+0.7328124642372131","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":"Q1073009$0D73BE7C-336E-4BE0-B853-8437806E385F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1063bece29dd4b6e998e94b2f0084b7f2a844456","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbfee5c07aeb327157f7563148d00892ea10b511","datavalue":{"value":{"amount":"+0.7258733510971069","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":"Q1073009$086562A7-A54B-4778-BF2C-A58BBA736E85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f8585afd9b3ca806c1c8b20a78c24b1a6a026a25","datavalue":{"value":{"entity-type":"item","numeric-id":5458380,"id":"Q5458380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ec51407ae871b1afa9784826830a8237e49de02","datavalue":{"value":{"amount":"+0.7098880410194397","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":"Q1073009$33FAE9D7-9887-431C-92C9-C704C63173C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07622c762984e431a24d8f00c8686c029fd4655a","datavalue":{"value":{"entity-type":"item","numeric-id":2457800,"id":"Q2457800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c3f7745f90826dc4cbcfb60399a4eb8f1fe941ac","datavalue":{"value":{"amount":"+0.7021875381469727","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":"Q1073009$7D58DD68-C440-41A6-A971-6A411F7BC208","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f690c858d760c02bc1c787b31957541644aed107","datavalue":{"value":{"entity-type":"item","numeric-id":2851948,"id":"Q2851948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed15b748cce3938f9e71afad46e06240b60beb4c","datavalue":{"value":{"amount":"+0.6991469264030457","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":"Q1073009$9E284FE9-353C-47E3-8F11-C6DA3FC64F70","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A note on Presburger arithmetic with array segments, permutation and equality","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_note_on_Presburger_arithmetic_with_array_segments,_permutation_and_equality"}}}}}