{"entities":{"Q286805":{"pageid":288572,"ns":120,"title":"Item:Q286805","lastrevid":60662604,"modified":"2026-04-10T18:22:01Z","type":"item","id":"Q286805","labels":{"en":{"language":"en","value":"Improving legibility of formal proofs based on the close reference principle is NP-hard"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585261"}},"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":"Q286805$E77821E9-BF3B-4E79-97AB-5C90A1CEB823","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3f5873839bd3ee8551ebff240d892dc07229acf6","datavalue":{"value":{"text":"Improving legibility of formal proofs based on the close reference principle is NP-hard","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q286805$1F3455CA-F10D-4E8B-8B0C-B2AC4E0C00C6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"649fbed88c57e165584b9751e39bce36b02476e1","datavalue":{"value":"1356.68198","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286805$3A60F42D-23E1-471E-92A2-CDDC766C1E01","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"91705e7e82173950109985f05602a2e2cc8516e0","datavalue":{"value":{"entity-type":"item","numeric-id":286804,"id":"Q286804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$FC9F6472-E390-4C01-9C1A-A85E70E22ABA","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":"Q286805$0CACF9CB-ADE6-4945-9F38-241471713898","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-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":"Q286805$60B12243-F19C-4858-BF28-29B444662EC9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286805$6FA9EF4B-E4AB-4ECB-8C8C-5B7D9D530A1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286805$796779BF-40BF-4047-B2A1-19D450A0B02C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8195a9e26c453276e1d31339bf2413392412013d","datavalue":{"value":"68Q17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286805$7FE37F5F-91FD-4781-97FE-4CAEBE57DE07","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0b037a0210e670afb6b3fb161b562e036ccedcb9","datavalue":{"value":"6585261","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286805$28D4CEE0-8B63-4437-8947-FB2B3C7CC48F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q286805$47E4D02C-34E5-45CC-BA59-1EE5AC941967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42c65a0055332c1201155c261f8526cf641db494","datavalue":{"value":"legibility","type":"string"},"datatype":"string"},"type":"statement","id":"Q286805$C212D84C-972F-4FF0-BFA2-98B4629DFBA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf1bbad404b660dcc4f7e1f74269a25b269f6b2f","datavalue":{"value":"NP-completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q286805$3B956697-203A-429F-BF7E-8E373F6D3B78","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$78FE660F-670F-42F0-BEFC-D2436690F5CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$7CF717EA-E10A-4E76-AF2D-CB603F036627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$770BC903-4608-44B3-9926-1BBC46886938","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"507c76a6be67bbc0f78898b0ad6ba2c059a645fa","datavalue":{"value":{"entity-type":"item","numeric-id":36099,"id":"Q36099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$2A001E5E-7661-4D97-8D0B-29E5F9470324","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$5D442B20-72A3-426E-8FF1-075B7CAFC684","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$9A3DA63C-4DC3-41B7-99B6-D24634E53F19","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":"Q286805$134A8BC1-B9CF-4645-A57F-6D49F4EDF509","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"f39bedd016652257067a6f4c09fe755491fb0587","datavalue":{"value":"Q59407604","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286805$509AA2E1-5A30-40AA-A1DF-2B11264A0FD4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e113fa5eb30b73ea7926f4f08fb83ad43b993b47","datavalue":{"value":"https://doi.org/10.1007/s10817-015-9337-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q286805$59A29886-1DE8-4815-9A24-CE39A7B5CBD1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4fa4a1f2ccb6c7848c5a275538b8fdf3e20702d7","datavalue":{"value":"W1268136390","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286805$DDB4C521-96A7-4D0E-92DF-567FA66ABEB5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"604f23db2dd4d34a2f60254ad57a8915830982b5","datavalue":{"value":{"entity-type":"item","numeric-id":5200114,"id":"Q5200114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$E8BF212B-47AA-469D-8CAE-492A8E1F41C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b06809062082b8f9f5dbc080e3987837376fa3d","datavalue":{"value":{"entity-type":"item","numeric-id":3499750,"id":"Q3499750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$BCD9AD3A-ADBE-47A9-9429-2E69639306E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836ad2a04f82225da478ca9f694f5cd99360b315","datavalue":{"value":{"entity-type":"item","numeric-id":4198056,"id":"Q4198056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$4FF14A28-9397-4E46-A477-73B818056235","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd2efa9cc52b9c7802bc3fd73236ab4bbd639fe4","datavalue":{"value":{"entity-type":"item","numeric-id":2921120,"id":"Q2921120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$0C5BFD0F-1F45-496D-80E3-967D80371C6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9190693f3924b86be7203c014f0b8b161bc6f8","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$02C3BD12-8828-4F7A-B224-22AC6AAE0DBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb1bab11b75e766c233c3a1b9a3682b90b0e288d","datavalue":{"value":{"entity-type":"item","numeric-id":3075247,"id":"Q3075247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$513F3BB8-6852-4658-97C5-2D1AC8E6E480","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7489ea30e71537d01eea3d2bdcb704e187c3f139","datavalue":{"value":{"entity-type":"item","numeric-id":5898511,"id":"Q5898511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$B049802A-2C86-478C-BC5F-A433EBAF9B7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"887efd17320625725aeddf6391561534d8fcc309","datavalue":{"value":{"entity-type":"item","numeric-id":5428273,"id":"Q5428273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$01B34313-1683-486B-82F6-B1DE3D1A9AA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37ee76102b0711d762453c86d361aa67599071c0","datavalue":{"value":{"entity-type":"item","numeric-id":5411648,"id":"Q5411648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$1653F27C-78B4-4C4D-9537-67B7402E308D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f585255e3cd65102bf6755b066e16e91ebc784da","datavalue":{"value":{"entity-type":"item","numeric-id":5259298,"id":"Q5259298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$6801DAEA-FF3C-41D4-9F74-903280F2C3C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5a256449611c84a11b081fc6ab121a5b321e50f","datavalue":{"value":{"entity-type":"item","numeric-id":1945902,"id":"Q1945902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$88B0D5D4-BF95-4C1A-836D-460C49DEE392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"692645ba0e13e1ab798946ded35053c7569206ce","datavalue":{"value":{"entity-type":"item","numeric-id":2907348,"id":"Q2907348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$B9F4E4F0-5FBA-496D-916B-889E9E07B8DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d8267b8b601e92bc0ef555ffe6911eece93f5","datavalue":{"value":{"entity-type":"item","numeric-id":1945908,"id":"Q1945908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$5667B4F2-A9EB-4734-99EF-6306D8CD83F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec41d91b97fe450aba006d86ee1b6e337fcab2ff","datavalue":{"value":{"entity-type":"item","numeric-id":5313068,"id":"Q5313068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$3143DED0-40E6-4D9F-ADBD-CFDD8959ACE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c852981cf03ba0205dbadf36200c00bb56793d8c","datavalue":{"value":{"entity-type":"item","numeric-id":3183518,"id":"Q3183518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$16FE8805-C56D-417B-B2D6-3849FC878F53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc4b8a556b0ebfab4e780293fc359a3bb7afe7da","datavalue":{"value":{"entity-type":"item","numeric-id":5852118,"id":"Q5852118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$25977678-12E1-4729-B764-1E0ECCFB6599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25f0acc466158a903ebc55021e2a6a9064d5094b","datavalue":{"value":{"entity-type":"item","numeric-id":4945208,"id":"Q4945208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$B91530AA-4F44-4E21-817A-EF4A0C9378D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae2da92fb913582a601af7173c06716220bbf7eb","datavalue":{"value":{"entity-type":"item","numeric-id":5898530,"id":"Q5898530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$A231975F-42FC-4C0B-9D43-583CDF7971D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"502ad8224b7ee39a96e36cfcfba1b8b740baa8c6","datavalue":{"value":{"entity-type":"item","numeric-id":4790672,"id":"Q4790672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$CD755BCC-865C-46AE-8094-8EF21631CEBE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2f252f09a698bc4c5ea1c1554160a3043bcbb414","datavalue":{"value":"10.1007/S10817-015-9337-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286805$A9776485-211E-4ACD-B65B-588CCC3B65CD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b3bd18569241bf72e66beb15708a3647d0bcf61","datavalue":{"value":{"entity-type":"item","numeric-id":2921120,"id":"Q2921120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09d0b3b7d0b081603c782adc58db605a1bfbc183","datavalue":{"value":{"amount":"+0.8572496771812439","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":"Q286805$E08FDD70-C47A-4653-A5DB-B55F2A4149C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"011f28f1bd0481f20174e5f049ee296de6638d11","datavalue":{"value":{"entity-type":"item","numeric-id":5495936,"id":"Q5495936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f1734a77698b51f4c0aa214fcfc4f181ee66391","datavalue":{"value":{"amount":"+0.8064905405044556","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":"Q286805$9B2AECE9-BDA3-4345-AD50-939560036B9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0520058733a5494928b7ed0f9d544740653dc701","datavalue":{"value":{"entity-type":"item","numeric-id":1945902,"id":"Q1945902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80e92b4f76ef52b7531f7098318202199bf6b19c","datavalue":{"value":{"amount":"+0.7185519337654114","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":"Q286805$ACE5F45C-E437-4210-9928-BAE2101F7DFB","rank":"normal"},{"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":"69c0e1adcdd34db7eaefb9f044f750c818c2c551","datavalue":{"value":{"amount":"+0.6945417523384094","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":"Q286805$A926E95E-CA50-47C1-B9E9-D4DD01CF0DC6","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":"2f4a195ed656169614c4990cd9c8b2b649f324e2","datavalue":{"value":{"amount":"+0.6932783722877502","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":"Q286805$29DC4C69-EF97-4B90-A231-DBE7A55F5829","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286805$E6EFF10E-D9DA-4431-B091-7CE8B31FAD0F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Improving legibility of formal proofs based on the close reference principle is NP-hard","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Improving_legibility_of_formal_proofs_based_on_the_close_reference_principle_is_NP-hard"}}}}}