{"entities":{"Q4988643":{"pageid":7018220,"ns":120,"title":"Item:Q4988643","lastrevid":54002375,"modified":"2026-01-26T01:46:07Z","type":"item","id":"Q4988643","labels":{"en":{"language":"en","value":"Refactoring proofs with Tactician"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7349320"}},"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":"Q4988643$2628DF7B-05A9-4FAB-BE3E-EEEE955750BA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"54eff6167dddf4d3b02dd556c49b475d6f2eee88","datavalue":{"value":{"text":"Refactoring Proofs with Tactician","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4988643$A527C239-8B5D-437E-9B85-3D0A4A8B6687","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"06039d14feb26783c212c6697bfdb038110e9727","datavalue":{"value":"1461.68246","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988643$77C30397-0B44-45A0-9DD4-73BCD3768577","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"505fb4b9ed464edb6f91bf5fe3e1408a475c79f8","datavalue":{"value":"10.1007/978-3-662-49224-6_6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988643$C0A7F7B8-8A05-430D-A1D1-684CBB9DEFDD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a8f5cbf6360429635db718a7502a7494a9026ef3","datavalue":{"value":{"entity-type":"item","numeric-id":3095231,"id":"Q3095231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988643$009E3537-6240-4A16-82B8-2E1315AE1004","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bdebb62d7a8887c495c6d5cbf51f30c9d6c5d73d","datavalue":{"value":{"time":"+2021-05-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4988643$8BB1A9D6-2AD0-4147-A61A-DF4EFE805705","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988643$DC0CA320-D900-4FBB-8318-96EA71F53591","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6faa4034d7fd1084b8d43ed64d8c7eb69a825835","datavalue":{"value":"7349320","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988643$A95FFFF1-06D1-4876-ABC5-4AE4195C873A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988643$E56DDC18-EEC7-4CDC-8CDC-72795EBE957B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62ba86aa6537435eabbaebc8bfe3b9fc42cedbd1","datavalue":{"value":{"entity-type":"item","numeric-id":29448,"id":"Q29448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4988643$F024CEB9-408C-4818-8C2C-95C2DD0530E7","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":"Q4988643$46D1DBA4-7590-476F-A9A4-862AB4B5D7E3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f1eea7fe85f8b8d479e85ff952e5c71e827079dc","datavalue":{"value":"https://doi.org/10.1007/978-3-662-49224-6_6","type":"string"},"datatype":"url"},"type":"statement","id":"Q4988643$5FCC50A8-ACF7-4425-8E7B-A2442608BC02","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b650e00651fcaeadffdeb5e886cea4686fa57c03","datavalue":{"value":"W2296387478","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4988643$A7486208-98FE-4EF9-BD3C-65C0178884FA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6802b362c841273e3825818c6b0ee2cbfeabcf6e","datavalue":{"value":{"entity-type":"item","numeric-id":5200123,"id":"Q5200123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8698134fe3b324765c79e838c386077d5a1fe292","datavalue":{"value":{"amount":"+0.8012872338294983","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":"Q4988643$54EFD706-9C3F-4B68-B2F6-6F2D87D11151","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68b122fc17cf6c180e33e2295f43b455fdd3224f","datavalue":{"value":{"entity-type":"item","numeric-id":2219409,"id":"Q2219409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce9cd212d47030c9b0964f05570172d7d701a6f3","datavalue":{"value":{"amount":"+0.7771928310394287","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":"Q4988643$889A762F-4763-4C65-B15D-36A2633D0260","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe7a7c4f5dac6dd56f6689fbd94d027549e0a9bd","datavalue":{"value":{"entity-type":"item","numeric-id":5756755,"id":"Q5756755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"154880ff2b41bf010b0c68aa226bf0f656754996","datavalue":{"value":{"amount":"+0.743325412273407","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":"Q4988643$7BFAA1A3-12B6-4E9A-9BEC-EF23374C3077","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d7c8ec3a59ef97be96d96d0177ee5b1e08031ba","datavalue":{"value":{"entity-type":"item","numeric-id":1341710,"id":"Q1341710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d55245916e5e2c1078261bdb404e247da6c5a80c","datavalue":{"value":{"amount":"+0.7251359820365906","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":"Q4988643$0476F51D-8081-4571-8C69-8CA5D8E05588","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d8229f7daafb1debae26fdffd7e93734038545a","datavalue":{"value":{"entity-type":"item","numeric-id":5210800,"id":"Q5210800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a872dc702d8ac863d9357a3a8bfd229dd7ec8655","datavalue":{"value":{"amount":"+0.7214480042457581","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":"Q4988643$F2191291-3195-42C7-BEB9-548C64AA9B3A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4988643","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4988643"}}}}}