{"entities":{"Q2828258":{"pageid":2838996,"ns":120,"title":"Item:Q2828258","lastrevid":52656269,"modified":"2026-01-23T05:06:56Z","type":"item","id":"Q2828258","labels":{"en":{"language":"en","value":"Decidability of inferring inductive invariants"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6642954"}},"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":"Q2828258$31A75DA6-C9B9-49B1-810E-329FD0A4B6F6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d6df4555901cc6872bd10d4a3550b230d4a8dfde","datavalue":{"value":{"text":"Decidability of inferring inductive invariants","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2828258$BA95E9B6-6B94-4C1A-9AF4-5D973F84F48C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9a48cb0074a40399f76027cc10b251137ca9af8c","datavalue":{"value":"1347.68234","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828258$A5BB1CF3-6404-4AA9-9659-68D1BD85E5BA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5242970313f4b97814e4313b567c49b421f711ad","datavalue":{"value":"10.1145/2837614.2837640","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828258$ABB477F0-4086-4F22-9147-EB4ED51354A4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"af28c01640955d451ab13d8ae854a3ea0fd656ad","datavalue":{"value":{"entity-type":"item","numeric-id":2044195,"id":"Q2044195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2828258$773B3BFF-3579-41B5-AB39-EEB9987FBB9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cec177c60e5a5e06c4135c2d656205cdaac4e3ae","datavalue":{"value":{"entity-type":"item","numeric-id":259064,"id":"Q259064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2828258$2DBC377F-17EE-44F1-B872-9F492CCAD865","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bc21e11847c1c83cb4b05afd906a2cc9c2cd1694","datavalue":{"value":{"entity-type":"item","numeric-id":671678,"id":"Q671678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2828258$AA5651B6-4FEE-4242-8F76-C7F2A913A8CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bfc7b1b7ab0184a05cf0cccf558a3e1b198b2a30","datavalue":{"value":{"entity-type":"item","numeric-id":2324193,"id":"Q2324193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2828258$2D9D83E0-2E21-44CF-936F-CE908B2ECC58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c9449ce466a2c684a15ed4352b5933311b5f46f1","datavalue":{"value":{"entity-type":"item","numeric-id":6482617,"id":"Q6482617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2828258$C7BF9102-628A-4959-930F-B0A1257A1F13","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0a99b403aab07b56f8645942f86d22ab58064aa8","datavalue":{"value":{"entity-type":"item","numeric-id":2828237,"id":"Q2828237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2828258$6A38A349-29BD-49A2-8321-0AD3BD4D621A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1a707999eca047eb3f3f8c2c26743b59dad9c97f","datavalue":{"value":{"time":"+2016-10-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2828258$9FBB0C02-4093-4450-B765-A920DD6269E2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828258$4F4579F3-D95F-4AD8-A121-8ECE900459F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828258$F268D949-9E70-4950-9D0E-F76811F8FC71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828258$907DC9CB-7FB7-4288-9EAA-B33B01221124","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3b89e757105f9bf797622ef15ca0fce5eae29fbb","datavalue":{"value":"6642954","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828258$AF7FAC4E-C476-47D2-A2EC-BB80E4F67972","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"104513d3dd0fe22d87f163bb45657059d03dab32","datavalue":{"value":"effectively propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828258$E5141CCF-E173-41C0-84C1-DC234BF65F21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b3d4a9a05b13366baf4389e80191c73fa1abc2d","datavalue":{"value":"invariant inference","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828258$BC6BD34E-3087-4378-833C-95F1838A57A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828258$41F3B3C5-DD48-4F00-BA0E-BBAE43E8E0FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dfd722232c4f35da3a742b7dd0939e8297df61c","datavalue":{"value":"well-quasi-order","type":"string"},"datatype":"string"},"type":"statement","id":"Q2828258$B612884F-4DF5-4114-9417-AF9E04676D2D","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":"Q2828258$D8BA0E16-1F7D-49C1-8C00-CA6A10709A96","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"70a7bfd4f6b51180a056f17c4c978ebe25d850de","datavalue":{"value":"https://doi.org/10.1145/2837614.2837640","type":"string"},"datatype":"url"},"type":"statement","id":"Q2828258$6AC7BB90-D861-4407-964D-0D5223B05048","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fb99ea811d093f72fa1e9c418e2f1a968129b5af","datavalue":{"value":"W2296031223","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2828258$124B1753-56FC-44DA-B1F1-E85A82D3794C","rank":"normal"}],"P1643":[{"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":"9c871845dedd821ede8cb1acc132cb485d9d8a73","datavalue":{"value":{"amount":"+0.7532193064689636","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":"Q2828258$80ED64BC-ED02-43E3-AD5C-E86C20766164","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca26097a05cbf4ea7f1980e0eae9fadc393cc59f","datavalue":{"value":{"entity-type":"item","numeric-id":4417916,"id":"Q4417916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4833a974896d6d339065621b8c8aa21b0bd75c2","datavalue":{"value":{"amount":"+0.7456684708595276","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":"Q2828258$2CE104C5-7A3B-4B87-9444-236E08FFF981","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6818cd45b997c627c00e90e817272a99221a2c1","datavalue":{"value":{"entity-type":"item","numeric-id":5716581,"id":"Q5716581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae21d0199319aef4a7d4e05ee79794176599f142","datavalue":{"value":{"amount":"+0.7441875338554382","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":"Q2828258$ABDF23BB-0943-49EB-8490-9B5EAF0A9DAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d82d52f705b6bd5ddd44d5eff9fee296a5bfaabd","datavalue":{"value":{"entity-type":"item","numeric-id":1702932,"id":"Q1702932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e192933c7895afe3f3b94fb31c9dfa83418bf66","datavalue":{"value":{"amount":"+0.7402251362800598","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":"Q2828258$87BBA819-8F79-48F8-9CA1-EBB456CA9B24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"948d5e4b90de55088042e1b5f1aa1157c6cc55a7","datavalue":{"value":{"entity-type":"item","numeric-id":2415375,"id":"Q2415375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a70300b1100a58c55e2f1c18721abe2eab25728d","datavalue":{"value":{"amount":"+0.7384052872657776","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":"Q2828258$FC965E96-D3F1-4E2A-963D-E01F119CEE26","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2828258","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2828258"}}}}}