{"entities":{"Q5958754":{"pageid":8135556,"ns":120,"title":"Item:Q5958754","lastrevid":40910759,"modified":"2025-04-14T01:30:17Z","type":"item","id":"Q5958754","labels":{"en":{"language":"en","value":"Reductions for non-clausal theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1715799"}},"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":"Q5958754$93F51046-AE78-419A-82FF-824C1B4CBEAD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"428b376077caab113c40e8f4b186f27a2340315b","datavalue":{"value":{"text":"Reductions for non-clausal theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5958754$A5B6BA50-E6DB-4BF3-94D5-004FAC063D96","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5f7bc7505177e255052dfe7f67984cd600b8518a","datavalue":{"value":"0989.68128","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958754$CC3AA52C-5185-4D6B-BA31-F75E744B02F8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ec76ad735d94f7de814b45170da314ed080c9703","datavalue":{"value":"10.1016/S0304-3975(00)00044-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958754$9EE518A0-B786-4A45-8630-9595A15D4577","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"92adb13e09b5aab7763bdddfde64b12a08209166","datavalue":{"value":{"entity-type":"item","numeric-id":236749,"id":"Q236749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$B2F54C87-A23A-4DF4-B9B7-D297A780DACE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7d4bccdf7c2b388b6e3e888805bc1f0030b29c7b","datavalue":{"value":{"entity-type":"item","numeric-id":1403341,"id":"Q1403341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$1343B978-624E-40AE-9FBA-13A5EBAF640B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"043b77db0c51d3789f284af5f275c7a673442b59","datavalue":{"value":{"entity-type":"item","numeric-id":587084,"id":"Q587084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$C0146FAB-D7ED-41FF-9BE6-1902B07A7B7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fffb11e3413fa5cc969a61a424e2554954849dc7","datavalue":{"value":{"entity-type":"item","numeric-id":236752,"id":"Q236752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$E77DC994-D394-4A03-A176-511373F7CCC6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$5466F355-449E-4DBB-A062-9802617FC37D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de0bbc1f0efc0eda52d8a37720ec217ae66c93cd","datavalue":{"value":{"time":"+2002-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5958754$F9493C68-0282-4227-A032-95119C28957F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958754$22E90D37-D2F8-4F07-A79D-340B7B95981C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"63b404419730055ce29869a4f88385a66c5f4302","datavalue":{"value":"1715799","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958754$95AB1779-9BC7-4EBB-89FD-1A1CC25B8BD8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c308e12360232ba96656b5c37f2a3bf5c43cf0a1","datavalue":{"value":"non-clausal theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958754$26305FE7-24EB-4336-BF9A-307EEF0FEDBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c115a59d8b8cbfdcfaa6b321f10fcc7cc4081cbf","datavalue":{"value":"prime implicates/implicants","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958754$84B3E3BF-D418-43E6-818B-F9ECBC202D41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"508def3536da451aaa16ab7a21353869c1e5bdc9","datavalue":{"value":"SAT problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958754$9168F0F5-F8CF-4EDF-B918-4809A5022730","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":"Q5958754$E792633B-6D07-4E6C-95D3-7C55F29D5809","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"85f836affe4a6b0b40172776244526a1f02ace4d","datavalue":{"value":{"entity-type":"item","numeric-id":4360107,"id":"Q4360107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$1D6F9528-6D76-40AB-B5F8-FED48EEF4C3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$8C248DEC-C157-4BDE-9538-722876430B30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9bc257831ae36e19142275c677c623b2a7c22c8","datavalue":{"value":{"entity-type":"item","numeric-id":4246976,"id":"Q4246976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$D6EAC167-95D3-435C-8B59-1B912903CAC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10e4ccae662a6738bca5b509ea61979b9dd23e26","datavalue":{"value":{"entity-type":"item","numeric-id":2674184,"id":"Q2674184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$9A53E286-B58A-40ED-99D0-B3AEBAE89564","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a0816d6f00a03a7666e63126256b4f78093a61e","datavalue":{"value":{"entity-type":"item","numeric-id":1379289,"id":"Q1379289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$0BEA86D1-4431-465A-8EF6-99216D873BC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f90f4bbf6bc7735bf0bedb03783935847e3cbf07","datavalue":{"value":{"entity-type":"item","numeric-id":3140015,"id":"Q3140015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$CC7D432F-F790-412C-99D6-D446A480F854","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb4ba955596cba8022ed29b088e14f54735c943","datavalue":{"value":{"entity-type":"item","numeric-id":1331929,"id":"Q1331929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$D2E603E3-6F5A-481D-AE7F-1BE60837C6F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eba87f647d350da9410e3009029b609261e32924","datavalue":{"value":{"entity-type":"item","numeric-id":5797033,"id":"Q5797033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$E3D29F41-C7F7-4036-B081-A2BCC92A6E83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8621ce0ae1e8c21956cfec192d952dd4054223f","datavalue":{"value":{"entity-type":"item","numeric-id":1111774,"id":"Q1111774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958754$2D8AC35D-1C36-4C23-B9D7-68D61512F577","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a606fdae945b1f049c48290fcb190a89a8a1204c","datavalue":{"value":"https://doi.org/10.1016/s0304-3975(00)00044-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q5958754$FE58CA8F-6743-4825-A980-86A088C626EE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9b6193d7e7d995d36ac1ea06dd7658de3abc235d","datavalue":{"value":"W2102501380","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958754$49E19533-5874-4EAD-B6DA-ABE7BF9978D7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb126188ae1240d08f769e6a040fc4f22ca0aa53","datavalue":{"value":{"entity-type":"item","numeric-id":2766990,"id":"Q2766990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d059404905cb9ab97daf0a76b200dbb3aa8170c6","datavalue":{"value":{"amount":"+0.89809024","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":"Q5958754$DC28408B-56DB-4FCA-9672-BBED564850D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7bc92e08faa2a642e2d8b65c07376e36b43f342","datavalue":{"value":{"entity-type":"item","numeric-id":435190,"id":"Q435190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d44a3ba2265bcc740a8cd3c59f8fbb07cd1da1c","datavalue":{"value":{"amount":"+0.88684374","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":"Q5958754$FB585A40-1876-4892-9E37-A42AACB343C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab8523f9fbdd0cb5d75658db58f361aefd862698","datavalue":{"value":{"entity-type":"item","numeric-id":4903716,"id":"Q4903716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64e6cfdb90d339fd249030768e0ce747b71c8b8c","datavalue":{"value":{"amount":"+0.88397664","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":"Q5958754$60141334-8FCF-4110-A985-EE3731768D25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81aca38709b78489bda3bf6c74cca69f198df488","datavalue":{"value":{"entity-type":"item","numeric-id":4644602,"id":"Q4644602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"857ba57341148f09044e132f45be8a57776c99ef","datavalue":{"value":{"amount":"+0.88103116","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":"Q5958754$2B10E7DC-F52A-4214-88F4-4B6B02C9E7A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e5657ef05db95b55c750ecc4436188bea089e73","datavalue":{"value":{"entity-type":"item","numeric-id":1799068,"id":"Q1799068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d01887c094bb2fab9b89087c4bf91a0e5c085fea","datavalue":{"value":{"amount":"+0.8786426","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":"Q5958754$ABAF6230-9CB2-42F3-8743-0B376AAD01CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7854d8d87637b7ccc5c885e4f2cbb2a7dfc6ef59","datavalue":{"value":{"entity-type":"item","numeric-id":2987064,"id":"Q2987064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46277916c8e91867ad95324092c706a16112f07a","datavalue":{"value":{"amount":"+0.8782523","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":"Q5958754$CA13FF03-EA8B-45E3-AF60-69D5213923D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0621ccfd9d5a431ca49ca46e528743876ccd438b","datavalue":{"value":{"entity-type":"item","numeric-id":4250044,"id":"Q4250044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9cb5990ef6029c88155d97e23e8a3cc65275b104","datavalue":{"value":{"amount":"+0.87741846","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":"Q5958754$3E09388F-595E-4826-8B56-F750C5BB8C77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb2237d5df6fc81179b573483e3885ede02944bc","datavalue":{"value":{"entity-type":"item","numeric-id":2351156,"id":"Q2351156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97b082924e3f0d812480330ab849d3966bb7cfca","datavalue":{"value":{"amount":"+0.8767158","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":"Q5958754$3689BE3E-F666-49EA-A28B-C0AD56E9B9D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0880741c3c12b53e29e3e6a1d6dce99a7cfef870","datavalue":{"value":{"entity-type":"item","numeric-id":5200021,"id":"Q5200021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97b082924e3f0d812480330ab849d3966bb7cfca","datavalue":{"value":{"amount":"+0.8767158","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":"Q5958754$48B875EC-0C4B-4CFA-A117-DFFCFB30E8AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9acf76d4282f666f48eda47b30cbeb51aa60e5f","datavalue":{"value":{"entity-type":"item","numeric-id":4809790,"id":"Q4809790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"20a05dc65b88f139713b3f1b9a537c361d2ad719","datavalue":{"value":{"amount":"+0.8758476","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":"Q5958754$82FD0AC1-E180-4A32-9E4B-6133D94CD53E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5958754","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5958754"}}}}}