{"entities":{"Q5450569":{"pageid":7480128,"ns":120,"title":"Item:Q5450569","lastrevid":50305250,"modified":"2026-01-13T19:13:57Z","type":"item","id":"Q5450569","labels":{"en":{"language":"en","value":"On Variable-inactivity and Polynomial Formula-Satisfiability Procedures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5248836"}},"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":"Q5450569$848922F4-1E2B-4835-AAF8-3F15BCB6F431","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9b971e8ef4479a26e52dd6e74e7eea9345f0f388","datavalue":{"value":{"text":"On Variable-inactivity and Polynomial Formula-Satisfiability Procedures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5450569$8E1B6D43-D5FF-45E9-A372-D3936469FF0C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c06b58a8dea899095862ce6a3191b5d8fa636e7c","datavalue":{"value":"1144.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5450569$4A01D3C6-DF00-4946-9006-55951397650D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b455290f5b835c3773a6eb2262897ac70e7a163b","datavalue":{"value":{"entity-type":"item","numeric-id":287273,"id":"Q287273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5450569$45F0C358-7267-4854-B547-91F0AA605C73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"da9d0bb1bba7f8d78f26f8b0456c3cbe905220ef","datavalue":{"value":{"entity-type":"item","numeric-id":438577,"id":"Q438577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5450569$CBE02214-CA38-4FED-BB24-61519A3E7191","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2bb6064fe12f1f98326de21fadc6a9704c90a","datavalue":{"value":{"time":"+2008-03-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5450569$93A73F8A-9C0E-471A-B711-304CA15842D5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5450569$2461D556-1C4A-4DDD-A280-6B95D1FEDCD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5450569$FAA3B569-F6F9-4D78-90E5-F7C7CB08DA4B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8d2898fa4e4feeda6f4ecf9c82da46c5a220156a","datavalue":{"value":"5248836","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5450569$1C878E64-59D6-4138-B442-5E9E7B112DEA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q5450569$B1E83D14-25FC-4167-8731-C1897FD58AC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"878262a8c375bee693f527aee7dc10cd86526db4","datavalue":{"value":"rewrite-based theorem-proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5450569$2AC8CD4E-5F60-47DC-A640-5842FCE654DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q5450569$8BB80FFD-72E3-423C-A49B-D00549594F92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b1e14dae32ffd15bf492e951039b9f4e22ebef5","datavalue":{"value":"theories of data structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q5450569$888B88BB-8D6D-4478-8688-1D025ADC968F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da9a74add422144b6e1c9091e2425318b6e1a01e","datavalue":{"value":"theory reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q5450569$292C1F6A-C727-42C3-9CB1-0E312E02F374","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":"Q5450569$A42319C9-502F-4A4C-B0AE-ADEC40C6E1DE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"557a09d721c938856faa29f456175c5051e7dece","datavalue":{"value":"https://doi.org/10.1093/logcom/exm055","type":"string"},"datatype":"url"},"type":"statement","id":"Q5450569$40EFE707-1B13-45F5-9D83-C0B2E4FE429F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e3608ae88b0a9b59ffb55d80337e70eb1c2650fd","datavalue":{"value":"W2113890674","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5450569$9E479C49-6846-4E4E-88E7-19D4A464AAE2","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"a028d75075f4897a5016bac7c7b74449d9db369d","datavalue":{"value":"Q118123663","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5450569$8ED30FEE-D6C0-4CA7-893E-859B61D26987","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"918f94d71554508db4605f71a761b5ecee1548be","datavalue":{"value":"10.1093/LOGCOM/EXM055","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5450569$CC0D2F00-A122-4997-9DE6-64D0CEC96D8F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9e6aedf3faf6964e0bbb1663882629f007284aa9","datavalue":{"value":{"entity-type":"item","numeric-id":2983390,"id":"Q2983390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5450569$35E72A76-FD67-42CD-B055-33C5573D97FC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf8622c562c05b951ae17878a9cdb0da17672413","datavalue":{"value":{"entity-type":"item","numeric-id":5277822,"id":"Q5277822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2afe0db1e71a7a2181a541375ff0254bc37c45b9","datavalue":{"value":{"amount":"+0.8692591190338135","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":"Q5450569$24882B69-541E-48AE-A47B-A1135BA8991B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a27f65171a16ec1255d72e9a05aaa54b77fc0c6","datavalue":{"value":{"entity-type":"item","numeric-id":2864358,"id":"Q2864358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc80ab91d7173a9401a50a9481efa43934e3e554","datavalue":{"value":{"amount":"+0.8569648265838623","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":"Q5450569$4C72316D-E8F1-4020-821D-0221A05A886C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dad5ec5c98775653bc18dff51fcba06acfae076a","datavalue":{"value":{"entity-type":"item","numeric-id":5491893,"id":"Q5491893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9198fb2e750d0a9fc9d84552a3240e6e6770f263","datavalue":{"value":{"amount":"+0.8307142853736877","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":"Q5450569$B97770BC-B2D5-4802-8DBD-81CA93D0C217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"344b7ce42afdc81a139cf848803148cfbbc3bed5","datavalue":{"value":{"entity-type":"item","numeric-id":3608774,"id":"Q3608774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1e5ca5f51b8472a035fe26580f4ae26568918f7","datavalue":{"value":{"amount":"+0.8070029616355896","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":"Q5450569$37EBDC86-617F-4CCF-8EF9-66C2208B0546","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5c58ba094084c62addce8231789deff838749d2","datavalue":{"value":{"entity-type":"item","numeric-id":2864524,"id":"Q2864524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40413ee6f4b44bc38f039400c21f13cc62ec8a5a","datavalue":{"value":{"amount":"+0.8046732544898987","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":"Q5450569$DAE4E2E9-153C-4EA3-9A23-ECA3B9243EEC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5450569","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5450569"}}}}}