{"entities":{"Q1369079":{"pageid":1379819,"ns":120,"title":"Item:Q1369079","lastrevid":77988770,"modified":"2026-05-06T10:31:02Z","type":"item","id":"Q1369079","labels":{"en":{"language":"en","value":"Structuring resolution proofs by introducing new lemmata or how to improve the readability of ATP-generated proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1071885"}},"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":"Q1369079$B46EBF64-DEB2-44FF-B0A5-B7199965DF26","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"976e3f81e5b667c21a4740dd96e7352f8f56e666","datavalue":{"value":{"text":"Structuring resolution proofs by introducing new lemmata or how to improve the readability of ATP-generated proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1369079$1D81F13E-013F-4BB7-A64E-B0F20D1C678D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f7ff98dec5337a0d7e115d7cb4d3afc4f46f1d19","datavalue":{"value":"0949.03012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1369079$17316337-07FB-4DA6-B5CC-B5C34D294C96","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"016857d2732c12246ddece45835b54085c514949","datavalue":{"value":"10.1023/A:1005890730317","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1369079$11F60BF5-5C26-4992-AE29-E65F55D59637","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0a1804acd81a416808dbff3d0f35ba940db52734","datavalue":{"value":{"entity-type":"item","numeric-id":1369078,"id":"Q1369078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1369079$763ADB41-4A0A-420B-852D-96C682479531","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":"Q1369079$307E1A50-7CCA-4E1A-A287-3F781AE4ADE0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee6dabe770d01c58d9d16642e2d2c925ba77d77","datavalue":{"value":{"time":"+1997-10-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1369079$C65AD841-1163-4C80-976E-67EB04BBA70F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1369079$E39A4EB6-39DC-49CC-BB42-7EE55749A0B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1369079$203F870C-F5A4-46A4-A230-1685968E2C21","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2bec8707d42035bcb698e2ab693575a244792485","datavalue":{"value":"1071885","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1369079$54446805-8BF3-41F4-8C72-86EAA6E49F4F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d51cfd72635f2d7153b996c978f5dfd4015a6a22","datavalue":{"value":"structuring of resolution proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1369079$BE329610-949E-4B6C-AC16-5A5B3B66602F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e29760637aa127ffdf15a219c82e4d343b68383","datavalue":{"value":"readability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1369079$E104D0DA-FBB0-4B8A-9CF2-DBA5D507BDD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d08b387045d5f32867613a079bade46bc7d1d2c","datavalue":{"value":"function introduction rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q1369079$C98BDEF1-AE45-4C64-BF4D-EFFF795E3AF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ef53676346e6df3d6ac14dc6516840cce309e599","datavalue":{"value":"reduction of proof height","type":"string"},"datatype":"string"},"type":"statement","id":"Q1369079$8EC0415B-DC87-4A7D-A46F-0DE2826271A5","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":"Q1369079$5231FE10-333E-4790-8B68-030A00094695","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6552a483dad45ff3525eb5e31707b24bbd17d15d","datavalue":{"value":"https://doi.org/10.1023/a:1005890730317","type":"string"},"datatype":"url"},"type":"statement","id":"Q1369079$DD907EEF-9EE2-4BCE-9A58-6958E1497158","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b30e29b1ac31a89c4dae5b7025f9d4232bbe4879","datavalue":{"value":"W1602927380","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1369079$C84B21B4-C3F3-4B63-B54C-53AD6005B10A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"275043e7e8c4e5297664f978b9aa57e55ead1d08","datavalue":{"value":{"entity-type":"item","numeric-id":3781732,"id":"Q3781732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bdf002bbb9e7d7e029b9996e4b2d37f588d09c48","datavalue":{"value":{"amount":"+0.7757219672203064","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":"Q1369079$F7F6F0B0-FCC2-4167-B2D0-20E934B7E376","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8a5d18780a3dbdb4959fbe9fb76a2b4792c26e8","datavalue":{"value":{"entity-type":"item","numeric-id":3490999,"id":"Q3490999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e04e3eed1ff19d86d025c10dad1d55c1674f551e","datavalue":{"value":{"amount":"+0.7423402667045593","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":"Q1369079$373AC3B2-28E2-4B72-BE93-B314DE7A6653","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc05adc331cde80814ea964cafa7ea00f9096f6e","datavalue":{"value":{"entity-type":"item","numeric-id":4364511,"id":"Q4364511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"093a0dc84a1f56bb035a4e6391d527c5611358ce","datavalue":{"value":{"amount":"+0.7376307249069214","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":"Q1369079$EF128084-1692-44B8-9F25-E9758CF76DD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9694ecc95cd17e581b722a875304301e52d8edeb","datavalue":{"value":{"entity-type":"item","numeric-id":5391528,"id":"Q5391528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5a13977274a41cc36a30dafb6e729b5657b45cc9","datavalue":{"value":{"amount":"+0.7123568654060364","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":"Q1369079$4C3B97CF-91CA-48DE-85B6-7B61AFC2B15B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81e7b855e3255ed7374e30f72b41f621223fc94e","datavalue":{"value":{"entity-type":"item","numeric-id":2417949,"id":"Q2417949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7285a6e64130f818b97235a2caf406749fbac901","datavalue":{"value":{"amount":"+0.7114566564559937","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":"Q1369079$B60E4E4D-12A2-4174-B13B-3D5C5D06F398","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Structuring resolution proofs by introducing new lemmata or how to improve the readability of ATP-generated proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Structuring_resolution_proofs_by_introducing_new_lemmata_or_how_to_improve_the_readability_of_ATP-generated_proofs"}}}}}