{"entities":{"Q3648730":{"pageid":5678636,"ns":120,"title":"Item:Q3648730","lastrevid":90442949,"modified":"2026-06-04T20:12:10Z","type":"item","id":"Q3648730","labels":{"en":{"language":"en","value":"Goal-directed invariant synthesis for model checking modulo theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5640966"}},"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":"Q3648730$8B6B2CA2-5F87-486A-BE61-6A180FA3A23E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cf7bd682ac4a2c9c0b663fd2b052368efa1b32ef","datavalue":{"value":{"text":"Goal-Directed Invariant Synthesis for Model Checking Modulo Theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3648730$398F511B-A437-45E1-816F-B45992E5592B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1ca5b72594984e892f6332419ec0bc01aba32104","datavalue":{"value":"1260.68230","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648730$CA29244F-753B-4BF9-90E5-ADF1F97569A6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"06a82c7f4ba5136b2ab339e1142f3454deb39281","datavalue":{"value":"10.1007/978-3-642-02716-1_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648730$681F0E21-7E3F-4B32-9B31-7CD4B8246D67","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"44f075398e4ccd740a9ac00697271020232935ff","datavalue":{"value":{"entity-type":"item","numeric-id":284229,"id":"Q284229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648730$32A3CDB0-4B9B-4D0E-B66C-E2FBF10504A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a648f5f5c43d7007feb24ddb34b99c77877b620","datavalue":{"value":{"entity-type":"item","numeric-id":219438,"id":"Q219438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648730$34F01DE7-3C6F-43B3-8938-5A11C741DDB2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648730$45B7670A-BFC2-47B5-88DA-11654223310A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b8bdd78fc222a44e05f767ee071ed0c7d623c0a6","datavalue":{"value":{"time":"+2009-12-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3648730$15FEDA22-0EC3-43B8-BC52-A0BFD3B7C3BE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648730$86E061E5-A562-4E72-84F1-9D710C934863","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648730$74A76FA7-3044-4E00-B598-4B07D24DAA86","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0ec41d30f2c295547b28beaf1a29f14d22792e05","datavalue":{"value":"5640966","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648730$C6B74DFD-DF67-40CE-964C-4BD2F1FAC474","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648730$DEB09561-2EBA-46C9-988A-2CBB92BD9384","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":"Q3648730$4EB356CC-2D6D-40D1-A2AA-EFD0725DEA55","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c9d907514cc23340249705d5b38d5d8b2fc1c698","datavalue":{"value":"https://doi.org/10.1007/978-3-642-02716-1_14","type":"string"},"datatype":"url"},"type":"statement","id":"Q3648730$A189560B-DBC0-4C17-BA00-1148334A9C0D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"56d1f4e003aa6832c0ba06ceff97b9c2e64d7dcf","datavalue":{"value":"W93625746","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648730$3C3E487D-C500-4BB8-A545-B38D655D4F99","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16f3946f85e87256de2c415f3cf1a294f0bc2ef4","datavalue":{"value":{"entity-type":"item","numeric-id":3081445,"id":"Q3081445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7b4ac0bbc74284ef03889739e1d7700f4a9dc83","datavalue":{"value":{"amount":"+0.8059809803962708","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":"Q3648730$62A4C8F7-01AB-4762-8E21-1267FA8113F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"501587f1d5024fdaf6c3718f9d2901ae36121df6","datavalue":{"value":{"entity-type":"item","numeric-id":939166,"id":"Q939166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"379d105abbbd09f63418dd87bd9a0d5c007b223b","datavalue":{"value":{"amount":"+0.7794047594070435","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":"Q3648730$0A772990-F0BA-4757-BB5D-03A317FB7A4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d950c362d3801fde912fba8bdf9587069d04358","datavalue":{"value":{"entity-type":"item","numeric-id":5452621,"id":"Q5452621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c334f57d20667dc1fce61a3a7f7fdd4013bd3ea","datavalue":{"value":{"amount":"+0.764404833316803","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":"Q3648730$7BF72E29-12F7-4203-A114-3CC17D2EA3D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a505f5185cc790a15e02721fd0da0e503f46206e","datavalue":{"value":{"entity-type":"item","numeric-id":3177887,"id":"Q3177887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b889ec127f06589a4ebf39ba4227b9b616b3168","datavalue":{"value":{"amount":"+0.7551835775375366","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":"Q3648730$806CDEB1-8C96-4602-8C94-4FEA31223662","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bccbf5fc3944a9c4a28f412cecb088c5b82edac0","datavalue":{"value":{"entity-type":"item","numeric-id":5900667,"id":"Q5900667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f2244d9e835cc218dc46b9eb303059653004d1c","datavalue":{"value":{"amount":"+0.7525649070739746","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":"Q3648730$87A36B9A-16DF-4D54-9E50-564F8F6DF83C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Goal-directed invariant synthesis for model checking modulo theories","badges":[]}}}}}