{"entities":{"Q3115173":{"pageid":3125889,"ns":120,"title":"Item:Q3115173","lastrevid":51421397,"modified":"2026-01-18T04:15:02Z","type":"item","id":"Q3115173","labels":{"en":{"language":"en","value":"Algorithm for PP-reduction a PC formula to the clause form"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6007814"}},"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":"Q3115173$B16EB2ED-5A19-4188-8D62-EAA0461681A7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ee2d58a20bed5d68b6ea1a14cdd804a63388b87b","datavalue":{"value":"1249.68203","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3115173$98FCDF3A-5929-4489-BEE5-DBF87801FCC5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7f1971c90a7507af8e1e04fb469535e20df68ff8","datavalue":{"value":{"entity-type":"item","numeric-id":3115171,"id":"Q3115171"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3115173$2B3A9B72-3645-4C65-AD9C-8C92B54CE871","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"32c1c5e30ed65a805cefb24544f5b2c9e8522b95","datavalue":{"value":{"entity-type":"item","numeric-id":3115172,"id":"Q3115172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3115173$F2FA6F9A-17E9-4B60-AEAB-527091D8EA14","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e99af83acc3a318038d75fa739ce30bed3a5850a","datavalue":{"value":{"time":"+2012-02-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3115173$73F5F99E-10FF-4F90-BABF-04A9505B3D38","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3115173$DCE3688D-D61F-41A3-9087-AFFFE90E7758","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3115173$7383C07D-ACCC-43CB-A67B-EF609FFBD66F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1a2684bbbe7665999322da6bdc338a374fefca95","datavalue":{"value":"6007814","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3115173$4D335A0E-74E2-416D-BB57-D2B12026B928","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3115173$FB832FDD-2191-4C2D-94CB-0E96D3ED6528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q3115173$C29CD829-DC0E-402B-AB3D-764D4DFA5FA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dbe8984db2bd5adea30d35faddaffd121773ef96","datavalue":{"value":"principle of contradiction","type":"string"},"datatype":"string"},"type":"statement","id":"Q3115173$CAC73521-50FC-4DD3-B37D-48285F2EEBF1","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":"Q3115173$69651030-9AE1-48EA-8CEF-2D06767AEE4C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3e476e8b83f9585570206cefe1255d6663a8fc4","datavalue":{"value":{"entity-type":"item","numeric-id":3745826,"id":"Q3745826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b99713deb97f06a529e4e67038636e3842938b6","datavalue":{"value":{"amount":"+0.7518466114997864","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":"Q3115173$E4167911-36FA-4880-BDFD-4A7EAA25C2FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd7f3731b78075daa894e98fe63ef686e3b32a9c","datavalue":{"value":{"entity-type":"item","numeric-id":809622,"id":"Q809622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40caddf112fe74ced797a7a7773de9e96b25479d","datavalue":{"value":{"amount":"+0.7498007416725159","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":"Q3115173$A1154B03-84CB-46E4-83CB-64C9488FDE83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d2e5dcfccf86ad82bb064a81d797295101701f0","datavalue":{"value":{"entity-type":"item","numeric-id":3434492,"id":"Q3434492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa95be74f027f153b561cb8f5fe144ef38fc1f5c","datavalue":{"value":{"amount":"+0.747608482837677","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":"Q3115173$F6871601-042F-4893-B6B3-9583B1D78557","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39835574666932a9f226413e82925155b1598e01","datavalue":{"value":{"entity-type":"item","numeric-id":3338214,"id":"Q3338214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"265d75b9bb1bcd7c973c39b4ff7b2420ff7adcf2","datavalue":{"value":{"amount":"+0.7197798490524292","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":"Q3115173$614D343B-E6A5-43FD-ACD4-DB013C4075E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"efcd782c72c8baec804be5d31c8790803418577d","datavalue":{"value":{"entity-type":"item","numeric-id":5457670,"id":"Q5457670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87936d20efc43d90e8c37d2a78734cdc4d94a933","datavalue":{"value":{"amount":"+0.7138276100158691","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":"Q3115173$256FF36D-6A7F-440D-B80C-E4D9B303D74D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3115173","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3115173"}}}}}