{"entities":{"Q1980482":{"pageid":1991224,"ns":120,"title":"Item:Q1980482","lastrevid":82351490,"modified":"2026-05-06T20:41:48Z","type":"item","id":"Q1980482","labels":{"en":{"language":"en","value":"Accelerating predicate abstraction by minimum unsatisfiable cores extraction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7392495"}},"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":"Q1980482$E464F4F9-DFFF-4B46-AE62-E926313E2E3D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a3b86c820a954c35e53edfb2c225fa1a50897493","datavalue":{"value":{"text":"Accelerating predicate abstraction by minimum unsatisfiable cores extraction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1980482$2A0A65AC-61E1-4E73-8E63-7450D6FCFE09","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a1c67ebf0c8e61c93a8127c19e582acbcae1f016","datavalue":{"value":"1481.68032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1980482$B1080599-329A-404C-A7D9-C86BDF19A8EA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"aa22f9f47e6ec596921cc974f542c3d0f86bc6e3","datavalue":{"value":"10.1007/978-981-16-1877-2_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1980482$742FB724-A356-45FD-9BBF-48AF5D8A0240","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f863235e0486892d9ce93a6016b2ad0d4e67076f","datavalue":{"value":{"entity-type":"item","numeric-id":764113,"id":"Q764113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$1E8FBD3C-55EB-4841-B9B6-10BA92A64170","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b1301a1e60a3d7d1bd7777c41b2e890e91d12b9a","datavalue":{"value":{"entity-type":"item","numeric-id":1980481,"id":"Q1980481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$1AD66D7E-D92A-4998-95EC-A9B693B1479D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2db8919a9beb6e9a81b9396842de8928328d5777","datavalue":{"value":{"entity-type":"item","numeric-id":781484,"id":"Q781484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$3C7DE163-A8D1-4DF0-8F74-169854C5F4A0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e0a34c566225983433f9006f15108b45d4850d41","datavalue":{"value":{"time":"+2021-09-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1980482$E5B3E7E2-6405-4B8D-AF8D-037FEA6255A9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1980482$BDF6C931-DCD6-40E1-A0C9-C4CC528FE7F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1980482$7ACD8AD5-66AD-41E8-9BD5-63739BAFA40D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cd80e9ade304e6b9b43fd50d0c3436276c3c217e","datavalue":{"value":"68M07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1980482$355644DC-8D98-479D-B45E-8F6A4348E0A7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bd142e51f655da76edd03acca0f71f644737e343","datavalue":{"value":"7392495","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1980482$3D2C2ADD-B6FE-4BB2-82D0-C82FE9F5ED27","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1980482$7BB86FE2-6CB7-477B-964A-F4121154F53F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1980482$EFC05D90-97B0-4963-A0A2-0A2E7FC42522","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9fb50508d9ae1a4b5b2525656ffbf4223c07463","datavalue":{"value":"predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1980482$B62E0658-0CFA-4981-A985-2949D7304C72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3978d2f31bc86b19c4025fe772ec1974bbd09669","datavalue":{"value":"Boolean satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1980482$89D56FA7-CB01-46DB-890C-CC303FFB9E7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61e107940fc8af51cc7098e6130e065bf51dacd2","datavalue":{"value":"minimum unsatisfiable core","type":"string"},"datatype":"string"},"type":"statement","id":"Q1980482$68CB2ED1-C754-4678-9567-8A1AEDD29CED","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":"Q1980482$319BAD6D-C1A4-40FA-AB60-C70CADEFD496","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ed0bead4845c58cb62a9c5d80db7573618b4206f","datavalue":{"value":"https://doi.org/10.1007/978-981-16-1877-2_1","type":"string"},"datatype":"url"},"type":"statement","id":"Q1980482$91F6CCCC-773D-4289-A910-DA35C5A7DF93","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ff11527d810141d623889ef9b66752facdeb0210","datavalue":{"value":"W3153030442","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1980482$1E2FDC96-7E89-47C5-A7E1-979E1A08A5FB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$49158970-813C-42EA-ABBB-46D33228FFD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10440edeb6411a5dffebd950ae30bdddc7f27e76","datavalue":{"value":{"entity-type":"item","numeric-id":1037642,"id":"Q1037642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$4E2BCE2A-9910-4158-9B76-D5B54C20B31F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c625dcf0809403f5b84f6d7cdfc8c33766e0658","datavalue":{"value":{"entity-type":"item","numeric-id":2471741,"id":"Q2471741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$46607634-F7D7-4D02-8613-57DCCBAC248F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53ace1ca00d0f981a30fb584f0d2f61bf11eec24","datavalue":{"value":{"entity-type":"item","numeric-id":1028724,"id":"Q1028724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$D0699243-9C86-4E4C-AFC3-71266BA1DF95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"055a8b99184593f13e46527bd7d965d30b729d5d","datavalue":{"value":{"entity-type":"item","numeric-id":1042194,"id":"Q1042194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$CE683AD4-0205-4ADD-8730-88CC970F1D35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33e61914e50345b341b28acb200abd5acaa24faa","datavalue":{"value":{"entity-type":"item","numeric-id":3007682,"id":"Q3007682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$F83FC017-5262-4236-8164-BEE152CA07B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2a719daf5fb0c0d7efb4db15da2d4a13f1a6fbd","datavalue":{"value":{"entity-type":"item","numeric-id":3164969,"id":"Q3164969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$6621F283-16F6-4B0C-A189-EF24789EB45D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8442b3257c9baf2249a39adfe9776bd190f72ec4","datavalue":{"value":{"entity-type":"item","numeric-id":3192054,"id":"Q3192054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$621FEA94-DE98-4679-B70D-A1B85BA4B8A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85a0da5461a77e3d1740266a13fa2f767ff2372e","datavalue":{"value":{"entity-type":"item","numeric-id":2815093,"id":"Q2815093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$7575E5CE-EBFA-4A3B-8F00-38BA4ED303CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d56f6a513ce4f5f5e1d80098982eebcf74efd23","datavalue":{"value":{"entity-type":"item","numeric-id":6108818,"id":"Q6108818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$0D76E7A3-96A0-4F0B-A108-8C10BE7BC8A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c619ee9c0ab726d6bee614d5a55e108c84c5f41c","datavalue":{"value":{"entity-type":"item","numeric-id":2181933,"id":"Q2181933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$4259248A-8C90-42E1-B8A5-23CB369394B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d12ec469fa2f759f0a487bd1fcbc5857905beddd","datavalue":{"value":{"entity-type":"item","numeric-id":2225120,"id":"Q2225120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1980482$8868C3DD-BBEC-4077-B1CD-B2BFE23A4EC6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8baa14e88319bb40aae8bb111e040434ebce5abb","datavalue":{"value":{"entity-type":"item","numeric-id":3007682,"id":"Q3007682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e09d878a9194f3e68a3f9ee13d22acb08e1e1802","datavalue":{"value":{"amount":"+0.8045130372047424","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":"Q1980482$CC8474E0-D2D1-467F-8DC5-98AD6C5C216A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1373cabe5746a8dd10b6ff4b8db85586af5ee1cf","datavalue":{"value":{"entity-type":"item","numeric-id":5325852,"id":"Q5325852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b39b3d3d542a9cd95178c29db61c5bca2870721","datavalue":{"value":{"amount":"+0.7813154458999634","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":"Q1980482$48DCA6B8-8EF2-4941-A74E-6497B44C5E1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"305314cd53c45094fbe0975e30108a02ae33267c","datavalue":{"value":{"entity-type":"item","numeric-id":5756585,"id":"Q5756585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7ccabd0dc787d0e24d50492c087d9168da76c42","datavalue":{"value":{"amount":"+0.7771036028862","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":"Q1980482$8554B400-A7C8-44A8-8BA4-BC539B0FC34F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"79ffa5ff30461cd51e0211fecdb41174f0327193","datavalue":{"value":{"entity-type":"item","numeric-id":5897055,"id":"Q5897055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6dd8c3f5c352858ac5c05e506a873bb56c1e717","datavalue":{"value":{"amount":"+0.7638894319534302","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":"Q1980482$4F8BDDB4-B416-4E36-8DBD-3DD75C1B8A41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22ecf35482c820335b7bb156abd38e35239984d4","datavalue":{"value":{"entity-type":"item","numeric-id":3510827,"id":"Q3510827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f7fd71f6efc7822283038d1c074a471b8df45aa","datavalue":{"value":{"amount":"+0.7517188787460327","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":"Q1980482$99F5E659-D8C0-49F7-B8C8-C28C98B174AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Accelerating predicate abstraction by minimum unsatisfiable cores extraction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Accelerating_predicate_abstraction_by_minimum_unsatisfiable_cores_extraction"}}}}}