{"entities":{"Q3079919":{"pageid":3090634,"ns":120,"title":"Item:Q3079919","lastrevid":51200081,"modified":"2026-01-17T05:12:48Z","type":"item","id":"Q3079919","labels":{"en":{"language":"en","value":"Verification in ACL2 of a generic framework to synthesize SAT-provers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5860258"}},"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":"Q3079919$398B7C0A-BFF8-42B8-9EA4-07671AE03179","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"187d7274ad4fdff2a0229bf632af10a184f0d026","datavalue":{"value":{"text":"Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3079919$D95E113D-19D0-4947-8677-5CA5280474A7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"84595ef6a9896ff5560d12626558ea125dbdd061","datavalue":{"value":"1278.68273","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3079919$16B43839-11C0-4DBB-A5BF-48097D0AD4AB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e463d2bd5f205d03ae96f3292c6dbe79571c5478","datavalue":{"value":"10.1007/3-540-45013-0_15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3079919$0418C7FE-B25E-45F0-8379-8081E0F8C8A2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"76b38168777167ff49199bd7f47bfebb8e51e498","datavalue":{"value":{"entity-type":"item","numeric-id":438547,"id":"Q438547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3079919$CC92FB6A-72FC-42EB-B8A1-D90D6262C278","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc442b6d258731aa6f56db3b1030762f889ec8e6","datavalue":{"value":{"entity-type":"item","numeric-id":417948,"id":"Q417948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3079919$36BC632F-DF54-4E3C-974A-84BCDC1A6564","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7ab7d4636d237c78cfef4f47fdbac4805f8a7b82","datavalue":{"value":{"entity-type":"item","numeric-id":438549,"id":"Q438549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3079919$A5E988A8-AD36-484D-A68A-2078B10E9AA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3c5989ab1028cea7e9ee7fb42127fc02a808a197","datavalue":{"value":{"entity-type":"item","numeric-id":438548,"id":"Q438548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3079919$21C4663D-26D3-427B-AFD0-6289B795DAA8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1b30e253b497c9ae83eb323a9f6b0623853ce927","datavalue":{"value":{"entity-type":"item","numeric-id":3079910,"id":"Q3079910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3079919$A1E5C71E-D5E1-43D8-934E-0DDBF1D0CF2E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"aaeaed951fddecc25ccb3e6e454be3a7c14119bf","datavalue":{"value":{"time":"+2011-03-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3079919$91157A0E-F4E6-40F7-8BDE-10B14532D980","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3079919$0D2A8132-9191-4BE2-8C42-CBA9A0A0404A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"80860d5b83d7684ce4b00e08ed60e6de8dbcbb4e","datavalue":{"value":"5860258","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3079919$E8DD6CC6-E996-4DB9-8083-D314603DCDC2","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3079919$B428826C-C9BB-4FB8-96F9-8431D9B1E75B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91dd7e13f71e3e62484b361def521e363c006e6b","datavalue":{"value":{"entity-type":"item","numeric-id":16380,"id":"Q16380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3079919$6274208F-5171-4B5B-8F45-87DB9E5ECA39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"36f5026b55bb5cc68aa4d2933cfba0f3ca08a59d","datavalue":{"value":{"entity-type":"item","numeric-id":21791,"id":"Q21791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3079919$B745FA99-4F94-4DBF-9CD7-D37D4412FEBD","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":"Q3079919$F83512B0-B39D-4A3C-AD3F-891B87027B8C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"acc02c13dec9c999c3654a3168dac6360128b2c4","datavalue":{"value":"https://doi.org/10.1007/3-540-45013-0_15","type":"string"},"datatype":"url"},"type":"statement","id":"Q3079919$B57A8D8E-8F85-4A62-9CD2-D4B35DEB672C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"16689fa5c5f0282f16e042f17585549b40f954db","datavalue":{"value":"W1562355818","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3079919$DE8C0259-A1B0-4C48-80DE-D4BDE5E1BA2D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea53f4d0daf48dd7127e69ca85211a01679fed0d","datavalue":{"value":{"entity-type":"item","numeric-id":2583288,"id":"Q2583288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30ade0447db44792cc2bcb27e833b46661fe7a37","datavalue":{"value":{"amount":"+0.9726107716560364","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":"Q3079919$426500FE-8792-46FD-BD51-01648314CAFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5ab12d6457ec42347bef47f7f7188cc8c836911","datavalue":{"value":{"entity-type":"item","numeric-id":2817909,"id":"Q2817909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c38e94c521591edb5fbbe6061f51fc26558f5e9e","datavalue":{"value":{"amount":"+0.7777676582336426","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":"Q3079919$F7E89E1A-DE82-4981-B720-4072B89DD175","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"117a8384df9f2cfd5c63b60924d56a8724ff3cff","datavalue":{"value":{"entity-type":"item","numeric-id":5179007,"id":"Q5179007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fcdcd343770b70c2192356a5402c192990c007fe","datavalue":{"value":{"amount":"+0.759484589099884","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":"Q3079919$C2B1FB98-612E-4D1E-9977-A0290DDB698F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32781204d1db0d50f0fed8e58f21ef2e924a069d","datavalue":{"value":{"entity-type":"item","numeric-id":5327347,"id":"Q5327347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1ef15827343af5b93f10ae60ca7bae3499f5835","datavalue":{"value":{"amount":"+0.7545208930969238","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":"Q3079919$A0F6AF18-C00E-40BF-923D-9623C3B76E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fd393998d5d8122f3f33d466692f819966057bfc","datavalue":{"value":{"amount":"+0.7493749856948853","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":"Q3079919$78DDD7A0-48D2-4DE2-B793-A564F9E9A7CA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3079919","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3079919"}}}}}