{"entities":{"Q784140":{"pageid":785989,"ns":120,"title":"Item:Q784140","lastrevid":64307127,"modified":"2026-04-11T18:58:30Z","type":"item","id":"Q784140","labels":{"en":{"language":"en","value":"A cooperative parallelization approach for property-directed \\(k\\)-induction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7228511"}},"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":"Q784140$01A57ECF-0394-431F-ACEA-A8F8BA2504FD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5a692a5e8093eeb02b0f7ed7f7a06d982c3deeff","datavalue":{"value":{"text":"A cooperative parallelization approach for property-directed \\(k\\)-induction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q784140$5D771C8C-13A6-4ACA-AD8C-B799A96265DA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a6375b4cb0cac0d351f4eb926b82fac4c39d6ed3","datavalue":{"value":"10.1007/978-3-030-39322-9_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q784140$4C964C49-D72A-48EF-A03A-92FF7C5DA84D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0946a618bb46938edb68aaca49138b9212c6eb14","datavalue":{"value":{"entity-type":"item","numeric-id":784137,"id":"Q784137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q784140$CB3FA3ED-CB5D-42E9-951F-4D2FD5A405B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8ebfd430f823a6478294286ff8c6d38b91b1861a","datavalue":{"value":{"entity-type":"item","numeric-id":784138,"id":"Q784138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q784140$8850EFE3-2A07-4039-B233-6BBD41A09659","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c1f6444d049d9c57fcfb1a50096c7c7e894d6dbb","datavalue":{"value":{"entity-type":"item","numeric-id":784139,"id":"Q784139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q784140$218EF94B-B3C2-4E29-B298-7E3EF4440E2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"66a480d2e9b29ea82a9b0fc72873fd6d8201d31c","datavalue":{"value":{"entity-type":"item","numeric-id":287271,"id":"Q287271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q784140$77CB6F5D-4432-45EA-84E9-7111443F8B02","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"367b52f871d6b5e824ee75b3e7162a8cd956fdbd","datavalue":{"value":{"time":"+2020-08-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q784140$851E9656-AF37-4139-B7FB-8D6D778FEE02","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q784140$D43BF984-B080-4A83-9474-752CAECE45C6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c0835ed2c7e1a07ff06372008e3c6c3c31a7a462","datavalue":{"value":"7228511","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q784140$618573BF-DE7F-44A7-A20F-46A27EB93639","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da5613d0d04ca4761bb018644ae7f4db90f6fcf3","datavalue":{"value":"parallel model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q784140$1B99E73F-C801-40F3-A9DB-AE196C1D6563","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da3f992ea7530129fc3b12deb036c0edbe481e7e","datavalue":{"value":"lemma sharing","type":"string"},"datatype":"string"},"type":"statement","id":"Q784140$3767FFB0-9A58-4497-98D5-C247AF4CD491","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"929503818b76064cd6ecd1ca7afa6fb2a29ab4a7","datavalue":{"value":"property-directed \\(k\\)-induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q784140$1C123993-6087-4A68-A675-B02EC181F489","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f7bdae318ddd2852a7e8e6456609f9603acb00d","datavalue":{"value":"IC3/PDR","type":"string"},"datatype":"string"},"type":"statement","id":"Q784140$3DA59CF6-14A9-45ED-A949-FE7465487F38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03f1ce721ffa5b2f36084f57048f17032077e128","datavalue":{"value":"Craig interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q784140$BEF45EDC-035A-4717-94D0-894C6588450F","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":"Q784140$5DBFC48B-B0C3-4D7F-A32F-6B3602367E5A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6cc06bd0d6979b2fc0647e6da2f8c53db6f8a41a","datavalue":{"value":"https://doi.org/10.1007/978-3-030-39322-9_13","type":"string"},"datatype":"url"},"type":"statement","id":"Q784140$18D56021-BC61-4C07-9374-068432E0811C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c9d49d86e06806ff296a4cb6d58d3d805daecffc","datavalue":{"value":"W2999604408","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q784140$1FE8E212-5E31-422B-A69C-69B61D8FB5CB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ffc202638374ea772190b3e3d3f5d32f56840118","datavalue":{"value":{"entity-type":"item","numeric-id":1978017,"id":"Q1978017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c4e6951d258a0a92368ea30f7d47b1ae18a3ecc0","datavalue":{"value":{"amount":"+0.85695153","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$C6280749-C832-4100-87DA-04B0DACCD8DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0fad1674c6d83dc31194cbf0f096419a4ed6ac1f","datavalue":{"value":{"entity-type":"item","numeric-id":1102766,"id":"Q1102766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54cd12e4229275f6313515a0b7d49cc7de5b4db2","datavalue":{"value":{"amount":"+0.83826303","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$A66EAE3D-F4B2-4AF0-87C0-B6B801CD9257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eaeb2aaeba4a86b3a8126913f2f4bdbd988194a9","datavalue":{"value":{"entity-type":"item","numeric-id":4229567,"id":"Q4229567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82a525c524a350215b9711556b02cb993579226d","datavalue":{"value":{"amount":"+0.83470863","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$18D847F8-2741-4B06-A6B2-19D7BFE56DC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6fc7d5bfd27f92cc7cf21826c6e13a615f73a1f5","datavalue":{"value":{"entity-type":"item","numeric-id":6488520,"id":"Q6488520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"420e4700c9dc83140bc1b08790e256b5df851242","datavalue":{"value":{"amount":"+0.83200186","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$5E871F00-C764-4526-A45A-59FBBF462396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f90d48d690e48fdf321ee2d3a912ecd028d2da3f","datavalue":{"value":{"entity-type":"item","numeric-id":5327362,"id":"Q5327362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e5cf379b1ff21641c489a698a39c35fbeb4198f","datavalue":{"value":{"amount":"+0.82896155","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$35B06349-C326-4610-A7F9-FC439492EAFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fce6076098d67bb5f9ba5840bbe6a3d424e12e9e","datavalue":{"value":{"entity-type":"item","numeric-id":5943113,"id":"Q5943113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"caed961e5ef0f912c31d57ed6854357f53692681","datavalue":{"value":{"amount":"+0.8212194","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$9993C9F7-6512-4942-85A6-BD831BCB515D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"718b07129f6850143af2474e1f77ff794e4aab8d","datavalue":{"value":{"entity-type":"item","numeric-id":1601867,"id":"Q1601867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e8184454b854f6767c21b5580b4f54d438a6cfb","datavalue":{"value":{"amount":"+0.8209666","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$E5B5CB86-726C-4FF7-8C5D-3A29F7DFF95E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e73e1f203d1418f4da64a61dfe1e3e5a07d59a90","datavalue":{"value":{"entity-type":"item","numeric-id":1778348,"id":"Q1778348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c4a83b0ff30b1435909053bf7c85893c1d474142","datavalue":{"value":{"amount":"+0.82074976","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$8C24E8A2-32C0-4479-8726-5939983479E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d22df9a8ab886bf4b1c86ef9d38e4d46a30dcc0","datavalue":{"value":{"entity-type":"item","numeric-id":280198,"id":"Q280198"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e3779e86b7f305c167734e8f9fa23758313db13","datavalue":{"value":{"amount":"+0.8202964","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q784140$74838399-54A9-4C30-8EE0-A7C785F56C14","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A cooperative parallelization approach for property-directed \\(k\\)-induction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_cooperative_parallelization_approach_for_property-directed_%5C(k%5C)-induction"}}}}}