{"entities":{"Q6852300":{"pageid":20610460,"ns":120,"title":"Item:Q6852300","lastrevid":84266657,"modified":"2026-05-14T10:09:09Z","type":"item","id":"Q6852300","labels":{"en":{"language":"en","value":"Checking linear integer arithmetic proofs in Lambdapi"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8165079"}},"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":"Q6852300$6DDF949C-0764-49CB-A53D-770BD8E18E1A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b3d217cf798cafe632d11d48c5c5dc2d86c2a1a6","datavalue":{"value":{"text":"Checking linear integer arithmetic proofs in Lambdapi","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6852300$6B28D7AA-891D-4ED7-8F55-9875C5F457C2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f77dfb3300bfe0c2b08bd17261a69ebfeb052b31","datavalue":{"value":"10.1007/978-3-032-04167-8_20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6852300$491AA224-3C22-438E-88AC-6CE6D5CDB779","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2888aac0073b1274aefc26a1535da8dd684f3485","datavalue":{"value":{"entity-type":"item","numeric-id":6844156,"id":"Q6844156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$4F94DA97-8B3A-4993-B0BA-01D948FAE660","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5a4b473513180cf93e4a8c86844a2c4dad9ce336","datavalue":{"value":{"entity-type":"item","numeric-id":820130,"id":"Q820130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$F9E38A30-1788-486F-B889-3E94E31DFB95","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4e2bc91f75e01209d6a7a4128f3012d483189e60","datavalue":{"value":{"time":"+2026-02-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":"Q6852300$858582F7-E8BA-4BF3-8059-55C99347F600","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6852300$95603DD1-EEFC-4DA8-8799-5E71C4147066","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ae2f4e9717dc72a20d2c4f17bdde30d85a417c","datavalue":{"value":"68T27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6852300$EA03802E-B525-4144-A237-3557BF684B8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6852300$431CAD6B-1565-4D55-802B-DCD4202699DE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"968063393939ace28f86156645b9dbca957e7003","datavalue":{"value":"8165079","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6852300$50620DB5-D718-49F1-A326-19CB0C39A6BA","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":"Q6852300$51345A65-E313-4533-B4C4-8DE7B9B34D7E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc37cf6bf1a4fd159f089028e999146e64828fa8","datavalue":{"value":"SMT","type":"string"},"datatype":"string"},"type":"statement","id":"Q6852300$C66D8C82-29CE-4357-875A-5EE4516196C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b02b52b936c3bf01919bdc22c1fd608c2fcf452","datavalue":{"value":"Alethe","type":"string"},"datatype":"string"},"type":"statement","id":"Q6852300$6F076B00-EB13-48D5-8661-E4B605570942","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97e440dbdf4e2e0e7ed379f5b792b2776387d3b7","datavalue":{"value":"integer arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6852300$5D386429-CC13-43E7-AD62-E067C9159AF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7dc3d3cba13d326bf073240715d4fed26d00c616","datavalue":{"value":"Lambdapi","type":"string"},"datatype":"string"},"type":"statement","id":"Q6852300$35DD53D0-FDE1-46A7-AC2E-3DE90042BA2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2f5f9fa7c99fed84610c34025a6959701496fde6","datavalue":{"value":"normal form","type":"string"},"datatype":"string"},"type":"statement","id":"Q6852300$707F28FD-9BE1-48DD-918F-7675ABB20DB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95b67bc981090b288e40939345a46ef449359586","datavalue":{"value":"proof by reflection","type":"string"},"datatype":"string"},"type":"statement","id":"Q6852300$4A80F616-0E66-4626-B507-3461EB5D43ED","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":"Q6852300$F2A7DF59-A04B-46C9-817C-8306497359B9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7123f84d6e4eb80889035fb4bfb02477147975ff","datavalue":{"value":{"entity-type":"item","numeric-id":6535368,"id":"Q6535368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$572C651B-07B6-4751-82C4-4FA57924C0F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20e8225b7fde56abf09e51400675a474f11c4844","datavalue":{"value":{"entity-type":"item","numeric-id":3612435,"id":"Q3612435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$E92E61DD-15BB-4C50-B40B-FEA209317872","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7570f17854b65d37d0fc6434e08ad95073499453","datavalue":{"value":{"entity-type":"item","numeric-id":6854422,"id":"Q6854422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$B0312EA7-0226-4FFD-98CE-5E32A43C73CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9978b7c4cc188e85861053a3341ddd6c9e61540","datavalue":{"value":{"entity-type":"item","numeric-id":6544119,"id":"Q6544119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$19C33E6F-177E-4EE8-983A-48A5DB489AD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f3f19634b415ce3c468072f394d5dd693518442","datavalue":{"value":{"entity-type":"item","numeric-id":6159937,"id":"Q6159937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$7C5714EA-5B4C-46A1-9AFB-BFD31D3EF524","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7932a7cbcff11de7c7386e3c2b0bcf82c8f46cc","datavalue":{"value":{"entity-type":"item","numeric-id":5756491,"id":"Q5756491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$CD600BBA-E668-410A-B968-FEBD76B2EF5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9e023b28912e7a083da0c1a3a943222492109c1","datavalue":{"value":{"entity-type":"item","numeric-id":7025200,"id":"Q7025200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$A046351E-34AB-4DD4-96E7-DDD2841123B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4910caf436e8c20e95f1863e799c479989c8e8f4","datavalue":{"value":{"entity-type":"item","numeric-id":2307624,"id":"Q2307624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$37B6E359-1D59-4BB7-B972-4B2E73716EF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34b87924f23be2e9cf6d7b6faa675b811f5a3d7c","datavalue":{"value":{"entity-type":"item","numeric-id":3612625,"id":"Q3612625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$A9C2419C-586B-4D17-9214-041A45619EF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a12c8e6968784fcf3cb8105db0edc338d9a5ec0c","datavalue":{"value":{"entity-type":"item","numeric-id":3192189,"id":"Q3192189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$74BDAE66-67D2-408D-8D68-A8842650F30C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9811e0f445518a60fcf8a88a2ec5cd76d23ab843","datavalue":{"value":{"entity-type":"item","numeric-id":5477649,"id":"Q5477649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$7618ABA4-1BA1-4A8D-89EF-ED6042387CB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$F79DCBCA-04AC-43EB-BBB5-9CE856C2AF13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"001b7d5445aa7045e4e7c2e085937e64f4e7883d","datavalue":{"value":{"entity-type":"item","numeric-id":6854398,"id":"Q6854398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$00B1E09B-74C7-4290-9CFE-7132E54FCF2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$E01A8866-BE01-4797-8224-94F153DE02B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"432347ebf7758fa5347be4c601bf2d08f68cb652","datavalue":{"value":{"entity-type":"item","numeric-id":2055901,"id":"Q2055901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$C2001C21-B1A9-4C6E-A4B9-F4BD377DBF31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61d2acfca0f5dfd32b373cf14812fef011284ac9","datavalue":{"value":{"entity-type":"item","numeric-id":2055877,"id":"Q2055877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$BAB445D5-8A52-464F-8AD1-03472850B2B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7da843fc35ebe015907494c69b23b63fc0a14ce3","datavalue":{"value":{"entity-type":"item","numeric-id":5200045,"id":"Q5200045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6852300$4ECEC155-207E-49A1-A320-B67FADFCD484","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Checking linear integer arithmetic proofs in Lambdapi","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Checking_linear_integer_arithmetic_proofs_in_Lambdapi"}}}}}