{"entities":{"Q1102766":{"pageid":1113518,"ns":120,"title":"Item:Q1102766","lastrevid":70097523,"modified":"2026-04-13T12:25:25Z","type":"item","id":"Q1102766","labels":{"en":{"language":"en","value":"A parallel approach for theorem proving in propositional logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4051045"}},"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":"Q1102766$9C10800F-19B7-42DC-B4E1-3D01BA69F681","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"682ab8012d2558c1da379e4ddd0f6036fe249730","datavalue":{"value":{"text":"A parallel approach for theorem proving in propositional logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1102766$7B5639B7-8C29-4CED-B087-41D923482028","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0bb17ea4d6bbe253d1f7009cf36b3493cfe7da95","datavalue":{"value":"0644.68116","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$CBCBB352-1771-46D3-B0D2-F56F0643A046","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3990b790cbf90e4bf57d6ce6a27710633760a9f5","datavalue":{"value":"10.1016/0020-0255(87)90005-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$F888E4A7-B851-40CC-BE87-CDA6DA6ED34B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"710b28dd1432a94b675888c75c7af24f7a3c4f6d","datavalue":{"value":{"entity-type":"item","numeric-id":808296,"id":"Q808296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$3082652C-9489-4CA6-9701-CE3C4BF40826","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"310c9202c9e546c674e15638e21da37cfcffb990","datavalue":{"value":{"entity-type":"item","numeric-id":1102765,"id":"Q1102765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$5C9D9E38-D4E0-4F24-AEC5-10E2C6E605F5","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c144f0fb88440afe4b13555aedcc8676a016b6d2","datavalue":{"value":{"entity-type":"item","numeric-id":70466,"id":"Q70466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$C025BB2F-E78C-48FF-B86E-B6E22F98BD2C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1102766$EB7D5910-3224-47C1-ACE8-51C0C3CE8CCD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"71152c1befb8507ca2079061f9a9d0061edfec20","datavalue":{"value":"The divide-and-conquer strategy and a pipelining discipline are applied to theorem proving in propositional logic. The strategy is itself logically complete and sound. Based on this strategy a parallel proof procedure can be constructed. With a pipelined execution model, we show that the processing time using our parallel approach to solve such an NP- complete problem is of O(mn), where m is the number of clauses and n is the number of distinct Boolean variables in the given formula. The approach is simpler than those using explicit inference rules, since the deductions are performed implicitly by only simple checking and deleting operations on each clause.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102766$1DA0DC57-7133-4666-9337-E7271FD3E595","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$EC8EBD70-3E5C-4BC6-AE4F-C52B4F742C96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$7F36267E-D6FA-40A5-87D4-AEBAD088AA6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$6979C338-1B27-4DEC-8EAA-517475B580CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1e903e68a16880f66ed79a0863889f1b2d3c837c","datavalue":{"value":"94C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$E272AF0F-BA4F-48D2-9082-D5A0071D1019","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$F7CB1CAA-2A81-497C-8D71-C79BDE0FC5CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"419d6f2b09c39920e34f63114ff159a2f0a01812","datavalue":{"value":"03B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$EF696FB6-A320-4FAF-98F7-2F1A4D61DA45","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c9b4dd3ac0dd9c9851cc71d4d0ca157d7a355e17","datavalue":{"value":"4051045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$EEE15875-A729-4AA7-A8F3-C55D16A7C583","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb1a6020dbcb9cb2c5731c3e9643fb58fd64167a","datavalue":{"value":"divide-and-conquer strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102766$A3FA694E-0A8A-46B4-B624-5DE409D989E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"612e8e9794104f416f1680c58a051761b7cdc76a","datavalue":{"value":"pipelining","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102766$382338FE-87A4-4A82-9A97-654830FBB8AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102766$153B6F27-1A1F-480D-B075-9610FAE597C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93c047fb19c5161b32c5245d5c8c28b4500157fe","datavalue":{"value":"propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102766$FBF68417-7543-4B24-A615-7D1ED6FC6F38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0488e2be231ab7f5307c3f5d3f81861c22540f1","datavalue":{"value":"parallel proof procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102766$94E718DF-B7F5-4072-9834-95AB4C2E63A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f5498ca3e7abb035a7212a6e68902ac2f3c0126","datavalue":{"value":"NP-complete","type":"string"},"datatype":"string"},"type":"statement","id":"Q1102766$DC99A0DC-B14C-4183-9BAA-08877DD23D59","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":"Q1102766$FCD16546-1993-450B-8E64-3A00BA8B0DD5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2bc4386c98427c57aa13caaba99b5b3015165a21","datavalue":{"value":"https://doi.org/10.1016/0020-0255(87)90005-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q1102766$635BA766-2BF1-4544-9DDC-83A0C5EC46F6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d5eb96b4207b8c2e7fafcd3922a27d0276e81b36","datavalue":{"value":"W1490800496","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1102766$A7A611E6-E417-4D65-BBBF-09A97D94204E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"08b8154126bb7dcff376a3fb5230eefc60388d66","datavalue":{"value":{"entity-type":"item","numeric-id":5652222,"id":"Q5652222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$03D27890-AB9A-4AF8-8BDA-C2F7E8571D78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$C3F332A2-D941-4731-B7D5-93AD7EE2265D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef757ecac8e00102e8fe2d81d7657ee3391ff698","datavalue":{"value":{"entity-type":"item","numeric-id":4138187,"id":"Q4138187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$4402D3C1-8930-402F-94D3-578BB1F31BBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4dfb9c15eb8582237fb4b4fbea1ff81538e5bf8f","datavalue":{"value":{"entity-type":"item","numeric-id":3216155,"id":"Q3216155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$E480E8BA-F989-406A-A101-1D63865B4DD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c52b21e2b050930655d553363cf317d38372f3f","datavalue":{"value":{"entity-type":"item","numeric-id":3885184,"id":"Q3885184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$E08A9D59-6051-4091-BFF5-2BA6D32FD787","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d9e735882f0114d9d1bd74d7bde93766d995370","datavalue":{"value":{"entity-type":"item","numeric-id":4065051,"id":"Q4065051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$3C9DFA56-447C-4EED-B070-2195265C352B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d88b59834b70b7f9220e322a0d6885d8a2d9636","datavalue":{"value":{"entity-type":"item","numeric-id":3318088,"id":"Q3318088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$8E5A2461-0211-4C55-A8D2-4C85382546CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$80E8EE9C-41E7-442F-BD4B-A72EC42803D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$626C009A-48AB-43E9-96FB-7B196350CF2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1102766$A6991E9D-29A2-43F4-B2FD-3F6CF3117EB0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7e33e9e995bb87c38170c19a9e8faceee834ff58","datavalue":{"value":{"entity-type":"item","numeric-id":808298,"id":"Q808298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9fe352bbbed5eca56bcaff3378ffebf7019e1b7","datavalue":{"value":{"amount":"+0.8502090573310852","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":"Q1102766$AFDC70C8-963F-4912-8C9E-4E3623B2FBB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ab0e67545c3b2a8b127661821d16878f3e304c0","datavalue":{"value":{"entity-type":"item","numeric-id":1357089,"id":"Q1357089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e6555a9dae52baa126ab788294c356c13d1c6cd","datavalue":{"value":{"amount":"+0.811130166053772","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":"Q1102766$1F5592E4-BE37-4320-9743-F9349270F3B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ffc202638374ea772190b3e3d3f5d32f56840118","datavalue":{"value":{"entity-type":"item","numeric-id":1978017,"id":"Q1978017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"082c1e228b250c7160b79a7fcaef81d2edca7fa7","datavalue":{"value":{"amount":"+0.8083680868148804","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":"Q1102766$9413D6D0-B697-497E-B470-194D89A73106","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd0dbf6de875b2deecc322a14efb9e5b03609ece","datavalue":{"value":{"entity-type":"item","numeric-id":3204066,"id":"Q3204066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eff2f582891baf8df15e60d156be7502414fe795","datavalue":{"value":{"amount":"+0.8038742542266846","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":"Q1102766$7DB71300-9F6E-464D-9B70-AE21B5F7D551","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a971cb69f3ee325b28cb4cd3052ed1093d23738","datavalue":{"value":{"entity-type":"item","numeric-id":1189725,"id":"Q1189725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"442b9afb2635800a0d1acdf54987047e80b2cc7f","datavalue":{"value":{"amount":"+0.790695309638977","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":"Q1102766$FDAFF5B1-384F-4A4B-AE77-3549CE9DF5CC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A parallel approach for theorem proving in propositional logic","badges":[]}}}}}