{"entities":{"Q4647541":{"pageid":6677122,"ns":120,"title":"Item:Q4647541","lastrevid":53320952,"modified":"2026-01-24T17:43:37Z","type":"item","id":"Q4647541","labels":{"en":{"language":"en","value":"On Shostak's decision procedure for combinations of theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001931"}},"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":"Q4647541$27181649-B501-422A-9C44-090BEB211517","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8fbad88c96cb4c56a6867628e4f367ca7b6113c9","datavalue":{"value":{"text":"On Shostak's decision procedure for combinations of theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647541$63394914-5CA3-44C1-9D85-78D41BC775C5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"521275c0ae71b50c815cfe914980c0d48cdfc6e9","datavalue":{"value":"1415.03019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647541$AFCA976E-A2DE-4908-9161-4F26DF13B18A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dfea3498013eea1e61cb657cce9dc8a38902a4da","datavalue":{"value":"10.1007/3-540-61511-3_107","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647541$94D83F7C-21AB-42EC-B281-E5BC93DC0C04","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"535627601f641e55f3cb47bf3f6e7f6def44834a","datavalue":{"value":{"entity-type":"item","numeric-id":1116355,"id":"Q1116355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$071E1034-F80B-4AC1-97EE-E558D7ACAE62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f977cc4afe30a7452131df7ff084411daffbbaa","datavalue":{"value":{"entity-type":"item","numeric-id":532428,"id":"Q532428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$11BCC172-DE79-48A6-8D04-8714CED3371B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6d0bbdada3c9be42b370691f727810aaafa99222","datavalue":{"value":{"entity-type":"item","numeric-id":1575866,"id":"Q1575866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$C9F601B1-8AFC-4942-BCAD-CC6273513F94","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$FE245A33-F0EF-48C4-8182-DE3484C8D483","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647541$631E3B30-9D65-4820-B633-265CEA4EB0F0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647541$2FD908EA-A3A1-4DAB-B4A5-AA00AE9BA49A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647541$97211944-9344-48E5-A02E-AF029E411399","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1281dd6b9c4f62144bc68cb09edbb6fe30760a8f","datavalue":{"value":"03B62","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647541$B6CDED12-63FF-459F-B505-E51B11B0FC25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647541$D31B9E04-62DA-4341-9153-E9E78C6E1B2B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"62b411aacb7e743ab9aa917174a87344b611970d","datavalue":{"value":"7001931","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647541$572807E3-F7DF-47BE-A4CD-81B83F70651F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"403c0223f8b71e5af2936036c4ff752c2714132a","datavalue":{"value":"equivalence class","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647541$51AF4611-B476-43DD-A10E-E1B4D5A267FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647541$F7AB694C-9FF2-46C0-AFC4-91A81345B8C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e13bc8441d7666d4310a93839316ebef38c603a6","datavalue":{"value":"prototype verification system","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647541$17A86D5E-CA68-4CF2-B7DA-8AA46A029100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"312ed6497197fe722552104318fb5c842ebebed4","datavalue":{"value":"linear arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647541$D258F0A7-A3A3-4E39-8094-A4C4B6422950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e29a0a1a089c1739ef594b8aa170de0991ebf7f7","datavalue":{"value":"proof checker","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647541$FAFD4B76-3241-48D0-843E-A81F6141E419","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0252b90583a3720591e1bcebade6d086a9b1ed2a","datavalue":{"value":{"entity-type":"item","numeric-id":40607,"id":"Q40607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$84492898-C464-48AC-806D-B7BADBDCE9DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$05AC3C81-601F-4384-9E2E-4A47F16B4139","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$E741107A-4D1E-446F-A9AC-4F63F163E1EB","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":"Q4647541$5D7D8720-3839-4524-81F7-75FE4E6C129F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7626e8a7a51cc77482d8a6c0ec667217a41040cb","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_107","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647541$2D01F2CA-E7A1-4CBF-A926-2B431E04D62E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"28288ac481ad8c4c601456d938ce9842c695b4ea","datavalue":{"value":"W1546619436","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647541$3128F1BF-06D2-4AB5-BF46-6EC24C083695","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$E90A3E98-0B99-415F-9104-DAA831429102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae19a70a8616a64987bb08271f6f085e5255b8c5","datavalue":{"value":{"entity-type":"item","numeric-id":3908476,"id":"Q3908476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$04B2C2E9-81D0-487F-B3BF-D4559979D8B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c091a6831cd5964be54b37dcb6712a7f5f803bfb","datavalue":{"value":{"entity-type":"item","numeric-id":4692514,"id":"Q4692514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$D64DF83D-2612-4BB8-A56C-B76BFA20759B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$F9384D62-6B95-4D48-982E-BE0FC0795523","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"975126c2667d6964e52988e556bf8223ff836bfd","datavalue":{"value":{"entity-type":"item","numeric-id":3883564,"id":"Q3883564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$6D3DC0AD-B2C7-4AB7-98F1-88BFEF3E97B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e7ba899fe6ebee4a099eb3b4d2314dded3c074e","datavalue":{"value":{"entity-type":"item","numeric-id":1202095,"id":"Q1202095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$CA5E642C-1090-4255-8F24-1FFCECB956FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d09db88e7db8de8a699f35dd014c509760be4233","datavalue":{"value":{"entity-type":"item","numeric-id":4157961,"id":"Q4157961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$59BDBBD5-C0D6-46F6-9871-157B23DD18B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7d23d752af51468669438a65727e2f56ea73491","datavalue":{"value":{"entity-type":"item","numeric-id":3766889,"id":"Q3766889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647541$9950E918-C0D7-481C-8243-8E6EEE480E6F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c7753b0ba6315f743e142b8c993760203261530","datavalue":{"value":{"entity-type":"item","numeric-id":4808733,"id":"Q4808733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9dd0a6ab73f8217340277f26b79637a84dac03b2","datavalue":{"value":{"amount":"+0.914149522781372","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":"Q4647541$EDEB8509-E12E-4776-AFC6-B4E78CA3D5B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71bee125ea54a8e54d6d488c54ec9675e6f5fb42","datavalue":{"value":{"entity-type":"item","numeric-id":5900552,"id":"Q5900552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cbb27a44c23a67c2baa050825badc47bc25de5a8","datavalue":{"value":{"amount":"+0.8484085202217102","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":"Q4647541$E71CA2BD-00D9-4EF0-912C-40C086826845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5a65013c33f602e6ce1784423a65269c11cc9f7","datavalue":{"value":{"entity-type":"item","numeric-id":2368951,"id":"Q2368951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"647e938c0ead777fcc08acb7e78ac7d1dd47cc39","datavalue":{"value":{"amount":"+0.8441574573516846","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":"Q4647541$8BCCFDDD-AEB5-47E3-A8EB-E5B573764C42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08d1ee2b76c1c506a32de616b0b55aad34b8a7a2","datavalue":{"value":{"entity-type":"item","numeric-id":4417954,"id":"Q4417954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb1a40092637b16672578b0b085bb219c10f2d7a","datavalue":{"value":{"amount":"+0.8436558246612549","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":"Q4647541$EBACA396-3D42-43EB-A5AB-09170CCA8513","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e1470a97030887b8d84f75ee646436a0f66f52b","datavalue":{"value":{"entity-type":"item","numeric-id":3766889,"id":"Q3766889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1cf5a68f26a8b0b043c16af2e4028c379f5d5a00","datavalue":{"value":{"amount":"+0.840663731098175","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":"Q4647541$DFB0E1EF-B7E4-47BA-9EAF-B863EF04B5A6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647541","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647541"}}}}}