{"entities":{"Q3454106":{"pageid":5233506,"ns":120,"title":"Item:Q3454106","lastrevid":88240664,"modified":"2026-06-04T14:00:23Z","type":"item","id":"Q3454106","labels":{"en":{"language":"en","value":"Towards the compression of first-order resolution proofs by lowering unit clauses"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6515518"}},"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":"Q3454106$9847326B-F460-4E00-875D-9CF5A0E1DFCD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8bbede6c3d1ba835ba4219e6a232153a2440ea82","datavalue":{"value":{"text":"Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3454106$FE0D0B4A-B5FF-411C-AC9C-4A99021797D1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"23aee40297150911b1518180ffe29a998107c9a7","datavalue":{"value":"1465.68283","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454106$5AF40C29-7BE1-4E21-AD55-D8130C96ECB9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8fdd55dd133456f0cbaf5396782e160ab2c96ea5","datavalue":{"value":"10.1007/978-3-319-21401-6_24","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454106$86F474DD-3987-4C89-813D-F24B1E243CE3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0fcf720142b79e597beeae1524d4e95bbee76294","datavalue":{"value":{"entity-type":"item","numeric-id":528558,"id":"Q528558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$195678DF-F51E-46E4-81A6-E1C255614FCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0365ec2945198187c9a57348ee998a5f73811baf","datavalue":{"value":{"entity-type":"item","numeric-id":523302,"id":"Q523302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$34C1391C-4ED8-4B42-863C-CF84C0F954BA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3cc4c7edeb37e5e3024aeff0de74501df6e066e3","datavalue":{"value":{"entity-type":"item","numeric-id":3454078,"id":"Q3454078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$10F7CE7D-FDDD-4E6E-BA7D-F68AAFF77E0C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f34c33daac76be2878f4eb0eeca7aa927e679a8","datavalue":{"value":{"time":"+2015-12-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3454106$3FC2096D-7312-4556-BBFF-6411D164AB13","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454106$DFDA23CB-5E4A-47EC-8A27-F0477EFC3AC2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8e7b310eab10f1fb4218a85f13adb6883cb7dd0a","datavalue":{"value":"6515518","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454106$133004DA-C477-45FF-B272-6E71EE132EBD","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$B44734FA-1F1A-411A-8371-3FCBCDA71FA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e436a6dc19a8ceb81ec55b5d8bc0dbe9bddbe586","datavalue":{"value":{"entity-type":"item","numeric-id":23853,"id":"Q23853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$C70952FA-6384-4748-AC4F-A5505C0D82B0","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":"Q3454106$28E71CDD-A783-457F-A7C4-26D884944C81","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"687433909a0ca8aacacf776b5aebde3077c67f4a","datavalue":{"value":"https://doi.org/10.1007/978-3-319-21401-6_24","type":"string"},"datatype":"url"},"type":"statement","id":"Q3454106$D4C66678-406D-418D-B3C0-73184671EB0F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a23b2fd55d0b5a49a2c587ec28d792b41659e381","datavalue":{"value":"W1438958698","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454106$A24C799D-8304-4A3A-925C-CF2B5A50F628","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"afdf61a0a2059e16b185d7a6b73df5a4cee605e4","datavalue":{"value":{"entity-type":"item","numeric-id":610791,"id":"Q610791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$2C4AD724-4135-4A44-98AF-8C2CDCAA3B00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b50b91f8311af786f0cf8a14635c242329f84cfc","datavalue":{"value":{"entity-type":"item","numeric-id":2851933,"id":"Q2851933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$B46954C0-9F0A-4B65-B15E-910C5C1D45D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b43a25ba24825d35a343ae255abd617023e5daad","datavalue":{"value":{"entity-type":"item","numeric-id":5200028,"id":"Q5200028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$DAEEC032-0B06-4D98-8576-AD004C634456","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ffd59f3b5cc711e02e1b8b90021028e3c7e8cbb4","datavalue":{"value":{"entity-type":"item","numeric-id":402115,"id":"Q402115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$76BE4CFD-974D-4E6F-8EB3-46E698EB684B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46faa8f9dd9d2db15375b6f86cd9184a54fb226e","datavalue":{"value":{"entity-type":"item","numeric-id":5505525,"id":"Q5505525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$CD824A32-6440-42BB-B750-04A846510247","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f518b506a2020973c95d779fe4901b4a5767fdb8","datavalue":{"value":{"entity-type":"item","numeric-id":3066113,"id":"Q3066113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$49458CEC-F9CD-4298-ABF4-2CE57468E899","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f3dbc47deccb64d887f982dbe2cceb2d9bd9b1d","datavalue":{"value":{"entity-type":"item","numeric-id":5391528,"id":"Q5391528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$61067614-14E2-47C8-A82D-B4DED0FCE11D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$FF4F4402-1DE3-4295-B244-A6A0246D4C7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e1a8094411c4c770dd370a45c2db874b8897938","datavalue":{"value":{"entity-type":"item","numeric-id":3066112,"id":"Q3066112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454106$4DB8C799-6B89-46B5-A104-2CE48E58F567","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36b1f31f0bb5689edb3b47bb744c18b5266f7c34","datavalue":{"value":{"entity-type":"item","numeric-id":2851933,"id":"Q2851933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5571d2a4144210a722f8edc7b6cf92590742bb78","datavalue":{"value":{"amount":"+0.8897686004638672","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":"Q3454106$1AC88968-16AA-4F08-97E5-6F48C231EAD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da142d350185a41280ffb301861d1ff6d39ef038","datavalue":{"value":{"entity-type":"item","numeric-id":5200028,"id":"Q5200028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb1b14e1446e18cc9f9f43fa9da4a6af062baa38","datavalue":{"value":{"amount":"+0.8345180153846741","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":"Q3454106$55611CA7-D8C7-4042-B8C1-10814D4F5CBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a63d7fe6af7fb615dd0ada14d74a7ffcad7f853","datavalue":{"value":{"entity-type":"item","numeric-id":1040776,"id":"Q1040776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb08a3ee0dd5487c129e23cff7fcfd3b04908c63","datavalue":{"value":{"amount":"+0.7515475153923035","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":"Q3454106$73181D90-59F2-4528-87E3-3C9CC724690A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c70c7c6cc56bc304adf4c26e41735c161bfeeaf9","datavalue":{"value":{"entity-type":"item","numeric-id":5178991,"id":"Q5178991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e64d5116f6352d78b7cea411f7295fe8894ef975","datavalue":{"value":{"amount":"+0.7443444132804871","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":"Q3454106$AF8459A3-60CA-4D74-8239-5A96D004F8FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48a3d434253ed919faa661b14e883ac27b635cfa","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f0b3ece4b7f3b851ca312a7a401e5c92c77886d","datavalue":{"value":{"amount":"+0.7353214621543884","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":"Q3454106$D67B4BF5-0D7B-4531-99C2-A816A439DCEC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Towards the compression of first-order resolution proofs by lowering unit clauses","badges":[]}}}}}