{"entities":{"Q972432":{"pageid":974280,"ns":120,"title":"Item:Q972432","lastrevid":50992127,"modified":"2026-01-16T03:01:38Z","type":"item","id":"Q972432","labels":{"en":{"language":"en","value":"Deciding effectively propositional logic using DPLL and substitution sets"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5711944"}},"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":"Q972432$43C6213C-85FF-48F2-8B19-73793AD5C812","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"008b9baf30d1e25102b7e7d4b41fd6f6248282b2","datavalue":{"value":{"text":"Deciding effectively propositional logic using DPLL and substitution sets","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q972432$EDC4000A-16E2-4A20-9E6C-976904C1048E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ab52aa72f74d8375d8188d531aa248ef2229bd37","datavalue":{"value":"1197.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q972432$00BD95AB-5732-40A8-A14F-D5E6BA3739DD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3acd164a581932de272304f0d70a966bc961c951","datavalue":{"value":{"entity-type":"item","numeric-id":784150,"id":"Q784150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$DC0E6504-29BE-4535-98BF-806E6B32D5DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"899468d0fe4ec0ae9c5ef91b63881ae72bf40a46","datavalue":{"value":{"entity-type":"item","numeric-id":438532,"id":"Q438532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$64EAA032-7D76-4974-9557-FD5A01ED2132","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3f1a755ad39b856fc5a2e4101b7c12f7b83c7256","datavalue":{"value":{"entity-type":"item","numeric-id":483050,"id":"Q483050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$64DDFA3E-AB4E-4CF4-8FA4-5931FC75B9DA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$5EEDD86F-2A53-421B-9F1C-78AED6877524","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"42e10e35ad52bbf92f1ddeac6dedccab922b34f1","datavalue":{"value":{"time":"+2010-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q972432$2BA1379A-1ABE-4CDA-9FA6-29F8C30EA5E4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6bcee1680474f45aa4dea1b443212041c7033e95","datavalue":{"value":"This paper introduces a DPLL calculus that is a decision procedure for the Bernays-Sch\u00f6nfinkel class, also called EPR. This class of first-order formulas provides a generalization of pure propositional satisfiablility and quantified Boolean formulas. The presented DPLL calculus is complete in EPR and combines techniques for efficient propositional search, such as Binary Decision Diagrams. The calculus works directly at the level of sets and it is opened up to efficient implementations based on data structures, with promising preliminary empirical results.","type":"string"},"datatype":"string"},"type":"statement","id":"Q972432$4367051D-5C61-4192-BBA9-FFDEBBA8C4F8","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"f47d936c4ff4164197e28a1ea38124145d11538c","datavalue":{"value":{"entity-type":"item","numeric-id":313005,"id":"Q313005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$B714CB1C-8FEE-456D-AA47-FA05DA250664","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q972432$CA8517FC-A8A6-4196-854E-86EEE33C03AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q972432$90A0E5D2-4BC4-4D16-915F-162360391696","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f73e8519b7917f3a24f3cfbe7175ce7b53ae8262","datavalue":{"value":"5711944","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q972432$D079C469-EC29-453C-A347-3F361920AEA3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f7ac674268224c9b1b4b60f07b959745a70f08d","datavalue":{"value":"DPLL","type":"string"},"datatype":"string"},"type":"statement","id":"Q972432$185D759B-6C90-4DE4-928C-06BDEF396521","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q972432$718FD4D6-E839-442B-BC8F-820ECB2CE037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7a5d828163d64278b1567f26ae1192fe1213ca48","datavalue":{"value":"BDDS","type":"string"},"datatype":"string"},"type":"statement","id":"Q972432$3F283CAE-5D7D-43F3-AAAF-93EC841DC244","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"104513d3dd0fe22d87f163bb45657059d03dab32","datavalue":{"value":"effectively propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q972432$FC14A843-1A4C-49FD-86FA-92BF2034B0BA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cea1b2cb84bb47ca577fcebf0f42420b207179eb","datavalue":{"value":{"entity-type":"item","numeric-id":16359,"id":"Q16359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$5438270E-B134-4AD7-BAEB-AD5CB95B2493","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":"Q972432$062EB183-0406-48F9-B455-0F71AA40AB99","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":"Q972432$DFAACC19-318C-44F6-90B4-D55C34649C0E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"12bcc66bda532177200b3fb0c4d7eaa12ce63609","datavalue":{"value":"https://doi.org/10.1007/s10817-009-9161-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q972432$339A6D03-FC50-4270-BE20-7FBBA8B132B2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8dba6f8dd6d9edece9b181d5046dcc6e1b71a40b","datavalue":{"value":"W1999468161","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q972432$64751430-ACC0-4B2F-ADA5-6EB13846B0B5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a602e09c88fdca5675da1ecccb188cb8f4370446","datavalue":{"value":{"entity-type":"item","numeric-id":2506489,"id":"Q2506489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$1B87CA3C-638F-4D4A-AE9C-DBF763B3ED16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98b850b043885273916728e7ea46c854030ea9cd","datavalue":{"value":{"entity-type":"item","numeric-id":5387921,"id":"Q5387921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$7B87F4E4-83EF-4E98-A199-7B321BA313B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac1293c449a4ec199dbf2381bd6d081ce1eb4f43","datavalue":{"value":{"entity-type":"item","numeric-id":2389629,"id":"Q2389629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$54925ABE-CFDE-43BD-82F3-45C5686EF0F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$3EE58776-0B39-4027-A5C8-31C722C02699","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0ecda2530a74fd3b958fc170aad75894016b80e","datavalue":{"value":{"entity-type":"item","numeric-id":3541720,"id":"Q3541720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$E7978DCB-5297-4C5E-B621-FC4315C339D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bf54fd52b3ae148a01d4229df0c1b5a1e68af7f","datavalue":{"value":{"entity-type":"item","numeric-id":3613415,"id":"Q3613415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$CEDF4655-9150-43AC-9FC6-04A399F7697F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0870e13c4a5dd2b1ec6ccf0eb8fddafbaa000d2","datavalue":{"value":{"entity-type":"item","numeric-id":5713732,"id":"Q5713732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$2BD849A5-B567-400D-9E6A-014253C4F294","rank":"normal"},{"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":"Q972432$6FCC9CC9-72C6-47BE-A0A2-380599D3BF17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ebba25ec6e30e98195fd89fc28af9b9ec829611","datavalue":{"value":{"entity-type":"item","numeric-id":2751377,"id":"Q2751377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$1AD6C717-561C-4A13-A223-3320BD4AE00E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4e6adf13c6408e6c2eebe9bb0eee05dbe30b987","datavalue":{"value":{"entity-type":"item","numeric-id":3524998,"id":"Q3524998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$1D2126AF-DEC1-4544-9D18-BC705E37B92B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d6e5a2ec66a572177ef7c34d7ff9e3c5a3050d5","datavalue":{"value":{"entity-type":"item","numeric-id":1157324,"id":"Q1157324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$07F7E239-F9A9-4FA7-982A-8E4F4D117487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f73dbcede27190cd2e561f92a6060d4f68d2ae5c","datavalue":{"value":{"entity-type":"item","numeric-id":3608783,"id":"Q3608783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$D6FD3F6A-CBE1-4467-83D7-1075B981DECB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49162db0a9f16ba8ff1d16d655987623c3c4c4d5","datavalue":{"value":{"entity-type":"item","numeric-id":3541721,"id":"Q3541721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$56887519-BA04-42F6-8561-A80E9F1ED7C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93d71c3b92ca55baa877bab542d89fc889c93f6f","datavalue":{"value":{"entity-type":"item","numeric-id":972432,"id":"Q972432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$8F1B482A-B5EC-4F86-812B-11F4BC883B49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34ee3280a4aba13cdbe3d7d1fc17418bf7b49fc9","datavalue":{"value":{"entity-type":"item","numeric-id":5493378,"id":"Q5493378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q972432$5673A7DB-D772-4318-875F-783B2B9757D9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bfe839f92ff902d4664423b4e70059704a0ac3b2","datavalue":{"value":"10.1007/S10817-009-9161-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q972432$AFCB3707-B099-4B0B-83E9-C004108A3906","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"606e6cff2905b99daa8b44a795a562fcbc6d8ef4","datavalue":{"value":{"entity-type":"item","numeric-id":3541720,"id":"Q3541720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81d6e906fd74294e91cf6632eb680724a896022d","datavalue":{"value":{"amount":"+0.9982579350471495","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":"Q972432$3DA4564E-3254-4202-881F-731501C3871F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47227c3ededf306d0bae5b081c3c2eaf0e20bdbf","datavalue":{"value":{"entity-type":"item","numeric-id":5312898,"id":"Q5312898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb829a9e2163830bcd3d504b35a7cb0098205ebd","datavalue":{"value":{"amount":"+0.7934339642524719","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":"Q972432$C9B63FAA-C8BF-43AC-AA84-093DD58DD8E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e47fa51543127b144699ea47ffbe93caf3f9b06a","datavalue":{"value":{"entity-type":"item","numeric-id":4708927,"id":"Q4708927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0680b268f17609abe3846733b8a7e4d89ebd15a","datavalue":{"value":{"amount":"+0.7642691135406494","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":"Q972432$D343B681-11ED-4389-A692-C0DE4B32EC01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f986ec0cbe86d1b57ee3714c8843e3131806eb5","datavalue":{"value":{"entity-type":"item","numeric-id":5900727,"id":"Q5900727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10b3c273c6b1487d46f90af6897456c98738855c","datavalue":{"value":{"amount":"+0.7624160647392273","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":"Q972432$1F3E9E93-1521-468B-BFA6-5529757E9938","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c98ea2a386d9f7bd44617290589043b97e5d3bd","datavalue":{"value":{"entity-type":"item","numeric-id":2389629,"id":"Q2389629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9552eeec56a32deacd6dee7910fb2f26117474aa","datavalue":{"value":{"amount":"+0.7525103688240051","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":"Q972432$FB1D5755-56E3-4128-8C69-AB4049A87324","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:972432","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:972432"}}}}}