{"entities":{"Q5177337":{"pageid":7206909,"ns":120,"title":"Item:Q5177337","lastrevid":58469577,"modified":"2026-04-05T08:49:24Z","type":"item","id":"Q5177337","labels":{"en":{"language":"en","value":"Extracting verified decision procedures: DPLL and resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6413636"}},"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":"Q5177337$4983FE1A-C147-4871-89D9-FF718E7AD8F0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c8a4747be500f1db5e67619b7ae86e0a469bff3a","datavalue":{"value":{"text":"Extracting verified decision procedures: DPLL and Resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5177337$FA9F6A76-07CE-40EE-8BD8-9DAD47D18AA7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"73b23f5cb6353f7078d1aeae7507c2192665ee1c","datavalue":{"value":"1448.68454","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5177337$696BC278-4FAC-4C42-87E8-E3EBB645FA3D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"feffbec96d83e86fe107b280bda99582a34818fa","datavalue":{"value":"10.2168/LMCS-11(1:6)2015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5177337$705916F1-EDD7-46F4-88EE-E32B8A970C7C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"56802c23e662b5a0028381459762dce10bc420a6","datavalue":{"value":{"entity-type":"item","numeric-id":234584,"id":"Q234584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$4328F4B3-89A0-4504-AD00-0F5B9A4D00BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"76f6aa7de6379af98579649d2dbfea63e0031e9b","datavalue":{"value":{"entity-type":"item","numeric-id":3178286,"id":"Q3178286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$F5968BD8-9D5A-41DD-906D-321E0DCDE852","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"59bdf3d36e9ce42e8810d203cfcd2e72a91b62c0","datavalue":{"value":{"entity-type":"item","numeric-id":724936,"id":"Q724936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$57D6C616-DB83-4A9A-8505-95791F64B001","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d06c1321f49508cea4a158e2ae71d33c1ecda72d","datavalue":{"value":{"entity-type":"item","numeric-id":693062,"id":"Q693062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$8008BE5B-D316-489E-865A-E31377595397","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$7F6B4646-72E0-4A97-976F-90BCB45EFF6C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"aaa340ae51925f6905d18399dfd97774b2ad90cc","datavalue":{"value":{"time":"+2015-03-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5177337$1DEF21B4-88EC-4459-8A51-5091D998E746","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b5a45183e221308c105d0df7a06438daaddc9c9e","datavalue":{"value":"https://arxiv.org/abs/1502.02131","type":"string"},"datatype":"url"},"type":"statement","id":"Q5177337$A57573E6-7C13-4321-9DE5-2572391D014B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5177337$649B0584-67DB-4BF4-91B7-97BC186F7873","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5177337$273CD54E-EB29-4374-878C-67E6CB94F4E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5177337$123AB21E-77B0-4B30-82D2-3F872037B731","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ae2f4e9717dc72a20d2c4f17bdde30d85a417c","datavalue":{"value":"68T27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5177337$73E49718-DF8B-4819-BC73-62D54FF6B220","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1a4dc81f7a589ae951fc227083ebaddb872db6f1","datavalue":{"value":"6413636","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5177337$697F91AF-C2B8-4766-B8EE-B5C219C97A51","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f7ac674268224c9b1b4b60f07b959745a70f08d","datavalue":{"value":"DPLL","type":"string"},"datatype":"string"},"type":"statement","id":"Q5177337$D9E58E29-F0C0-427D-9772-8B9BD7EE4C5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5177337$E2880FDF-63E1-412E-9EE4-324D52FBD723","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5177337$B6AE2889-5DE7-4FE6-811A-326373828D1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q5177337$13E7AF27-AB0A-411D-896C-1C7A93384AD8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"179af68833d4e59c1e0a3c7b1bf054d82b9a6b91","datavalue":{"value":{"entity-type":"item","numeric-id":20426,"id":"Q20426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$008A5EC5-E1B7-4995-B49B-1DCA47264679","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e603d7c91a5659a0e67ae5a0b1fc4700fb0830e5","datavalue":{"value":{"entity-type":"item","numeric-id":31834,"id":"Q31834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$2EE6AAF4-8F49-4F0B-BF2B-4AAA0DADF643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$9A3B5720-76C5-4335-9D56-0353B614B3F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e3a7f5df06b272bd42f74baffc8ceda01dfacc5a","datavalue":{"value":{"entity-type":"item","numeric-id":17043,"id":"Q17043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$FE0FD1AE-5081-489B-9BDA-6A96ECA3D743","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$17EF3671-3D06-482E-9828-FAAE34B1B5BF","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":"Q5177337$D7D79C80-78AD-481D-8450-0AC17F32109F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$6804EDD7-C96A-4243-A036-41DE4156A452","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6e1a240c321e56a4c4972fd8e23ea8cd8e21bff0","datavalue":{"value":{"entity-type":"item","numeric-id":21744,"id":"Q21744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$B17F06B2-49B6-4AA5-9856-C801BB0CD94E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$DD2DFFB4-6B9B-4163-A827-DDE3199CE957","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$3D42211C-BC7F-4689-B5D0-1694297B17E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5177337$72A56C46-08CA-410A-9F9D-CC468BD36DFF","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":"Q5177337$51DCFC63-5508-4D24-91A3-9814CC83FF91","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45d4a06ef86ca1f117df35c39655a16ae19e64e6","datavalue":{"value":{"entity-type":"item","numeric-id":3178287,"id":"Q3178287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ae4e58af3a14991e611b5319082e517098a855f","datavalue":{"value":{"amount":"+0.9005371332168579","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":"Q5177337$B4A4A9F8-B002-4418-ADB1-DEF6CC9A8BFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4821d184ef83e5752c967d173acfc4a04c2e4cff","datavalue":{"value":{"entity-type":"item","numeric-id":5434504,"id":"Q5434504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee195e70b17033df4b55f3ef53db965a937be004","datavalue":{"value":{"amount":"+0.79884934425354","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":"Q5177337$D68D4169-6192-4E50-8D5C-54B145FD4405","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebc099bf621adc8a302704653b45f0029a43f506","datavalue":{"value":{"entity-type":"item","numeric-id":636273,"id":"Q636273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35774bc55f853dceffd096d75c8081b939890292","datavalue":{"value":{"amount":"+0.7987407445907593","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":"Q5177337$852742C8-D326-4E42-BE15-9503EE7C6627","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":"bbc45e90a4c08198cede524a32d09e2375a6708b","datavalue":{"value":{"amount":"+0.7758868336677551","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":"Q5177337$4999FEA5-A3FF-4BC4-8597-37FB6EA5328F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ad1ae46a13dbdff43b01ae1250f32f6cb7d67ad","datavalue":{"value":{"entity-type":"item","numeric-id":3562927,"id":"Q3562927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5c671ef764d2f7901393aa4d83c2d538be40f30","datavalue":{"value":{"amount":"+0.7715677618980408","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":"Q5177337$57624DE2-F877-4444-B50E-7BC0ED26BB15","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5177337","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5177337"}}}}}