{"entities":{"Q1799131":{"pageid":1809873,"ns":120,"title":"Item:Q1799131","lastrevid":53239799,"modified":"2026-01-24T12:59:52Z","type":"item","id":"Q1799131","labels":{"en":{"language":"en","value":"An abstraction-refinement framework for reasoning with large theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6958129"}},"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":"Q1799131$AD90BBAF-C1B5-4CFE-9944-1D28961EFE80","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1cdc97c4b17ce45e0266d8485228e48a72a19827","datavalue":{"value":{"text":"An abstraction-refinement framework for reasoning with large theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1799131$A77B7735-8257-47A2-A93E-B4E7D8F64717","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"53ea52c020f6fe82178b54e56e2a5ee2d8a703a3","datavalue":{"value":"10.1007/978-3-319-94205-6_43","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799131$735E9C13-EB55-4AE0-83A1-ABF886BCF085","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e3e73a7215ca696ecd3e0fc0f05e45b6e5f4dc1e","datavalue":{"value":{"entity-type":"item","numeric-id":1799130,"id":"Q1799130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$93BDB86F-1793-49B8-89E8-74E98D392201","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce9e1735095a7237c0c699c31f4c0eb57566d709","datavalue":{"value":{"entity-type":"item","numeric-id":1401931,"id":"Q1401931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$2328B9AF-BB44-4778-A2F4-AB33563D9015","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0172cdede3f306f1b36155a82f67164814fd11e5","datavalue":{"value":{"time":"+2018-10-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":"Q1799131$F03501A1-AED4-48BB-8B21-EBB6B5A5B5FC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"144bf49d096909b5b87d519ec3fb17d096a95920","datavalue":{"value":"http://www.cs.man.ac.uk/~korovink/my_pub/abstr_ref_ijcar_2018.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1799131$C3F9493B-9C43-4A74-B19F-9E951852F388","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799131$D14DBC2C-A586-42B9-AC5F-B9F8733F6C8D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"070be239bda8526ef9edc47ca064476c3487a869","datavalue":{"value":"6958129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799131$23DDD5D1-8EFE-4EC2-94B9-C6A4DCC2955C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799131$63A8478F-062C-40E5-87A8-0CA2D235BCB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c1f2ad05756145a4abf98a4573dfef14fdf354b","datavalue":{"value":"large theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799131$76B7E239-AFF6-442A-9DBF-55651BCF5575","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9917a2dfd376250c18f9925b8d22d45575bb3eef","datavalue":{"value":"abstraction refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799131$77EBFD4A-793D-41CC-AD6C-9113C4B1AE22","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$601AEE96-EC0E-4819-A298-33F570DE22C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8617a61c90a632f23d3851deb94e1069d2479a78","datavalue":{"value":{"entity-type":"item","numeric-id":13268,"id":"Q13268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$D2D8817D-AAEA-4C9B-A327-623F6299B130","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$E03EBACC-79A0-40EF-BB2E-828C4AF18B40","rank":"normal"},{"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":"Q1799131$D3852C81-F29C-4F00-9F6C-7BD9DDB48D4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62af2c5e450adf37bd9acb47c5a55b60b68447ea","datavalue":{"value":{"entity-type":"item","numeric-id":22241,"id":"Q22241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$5463F6CB-5748-4B5D-A4DA-85ABE6A69055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$5F3DEB8F-A3F7-4663-92CB-9EC004D5BE73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$FD30571C-7E50-4BBB-AE3D-A8E26B83DC0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"83e2dec25ea583652d0e07d4393a843812f4b48b","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$ACE7D174-A4E8-4671-A48D-C9B5966F02B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"23f1d4970d4f2ba01b8146500b5c1a10ed17d235","datavalue":{"value":{"entity-type":"item","numeric-id":23493,"id":"Q23493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$8182E149-DA22-4064-9978-601203CB3A48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"12995736fe82d65918938fdd42b1d647f84d490b","datavalue":{"value":{"entity-type":"item","numeric-id":33178,"id":"Q33178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799131$D5E149A7-1BDF-4ED0-882D-5CC4BCB0A83F","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":"Q1799131$9971DF0B-CB9C-4EB8-AD25-80F48A3F6E94","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8ea86253f64827c92c8d98617e86d285d7c2ee69","datavalue":{"value":"W2809879880","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799131$A098A5CE-A1EF-4D7A-BEEC-318F6F09180B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5153f4ee260d21542ec2b89d7787fd721bba360e","datavalue":{"value":{"entity-type":"item","numeric-id":3490995,"id":"Q3490995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33e027ab46a9088a6756c74b853bc44a0d633865","datavalue":{"value":{"amount":"+0.7553582191467285","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":"Q1799131$358DDCE8-939C-4152-8124-F623B5A13F93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"575bdc59d4732124a28b6b9f323d2d8636895b78","datavalue":{"value":{"entity-type":"item","numeric-id":5200032,"id":"Q5200032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7cccd18a8b1c86a8b975524183e8593bc103677","datavalue":{"value":{"amount":"+0.7405397295951843","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":"Q1799131$D40DA8D6-E0A2-4379-BDCE-53C08F1E47B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"349024f45525c8fe7c210fa555e3f89353510a03","datavalue":{"value":{"entity-type":"item","numeric-id":4263169,"id":"Q4263169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed7d893df088dbcd05b50bf5ddccb44335dbe677","datavalue":{"value":{"amount":"+0.7159935832023621","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":"Q1799131$11CB585A-2D6A-42B4-B3D2-260CDFAD2FDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92cf4a098c4740b58a63a324276145b1e9ddbc66","datavalue":{"value":{"entity-type":"item","numeric-id":4028090,"id":"Q4028090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1a4b25b06752bb9678e6de1aaeb94c1acd12ec5","datavalue":{"value":{"amount":"+0.7155437469482422","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":"Q1799131$F38A9560-94E3-4D75-8D64-DF6E0B7D9303","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09d72b2a5a9fb1810d850b52fcfccb7bfaba9d8b","datavalue":{"value":{"entity-type":"item","numeric-id":2964472,"id":"Q2964472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1a4b25b06752bb9678e6de1aaeb94c1acd12ec5","datavalue":{"value":{"amount":"+0.7155437469482422","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":"Q1799131$CD36F098-FAB7-4B7F-9165-3F17C0E4796A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1799131","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1799131"}}}}}