{"entities":{"Q6844157":{"pageid":20561641,"ns":120,"title":"Item:Q6844157","lastrevid":84281807,"modified":"2026-05-14T14:56:17Z","type":"item","id":"Q6844157","labels":{"en":{"language":"en","value":"Reconstruction of SMT proofs with Lambdapi"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8172633"}},"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":"Q6844157$05074B69-1E05-4ACC-BCFC-84FB5FBF0395","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b71f2172bf63e0fec424c4cdf08d0a194e2a3552","datavalue":{"value":{"text":"Reconstruction of SMT proofs with Lambdapi","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6844157$CB552EA8-FF7D-436F-92DF-2B45258A8667","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8b87e4f32fcd9929c68034c830ea281aa1daf13d","datavalue":{"value":"10.1007/S00236-025-00515-W","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6844157$C173760B-CA03-492D-9838-2EF3B738F755","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":"Q6844157$2114666B-52E1-403D-918F-7C77326F1834","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c0270c5f09013fd16c6b2445a8928308c49d0b14","datavalue":{"value":{"entity-type":"item","numeric-id":608193,"id":"Q608193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$C102CBEB-943F-4011-A46B-7B578928C6E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"20dd65c281e6e985b6ecebe81cd888c922b7f37c","datavalue":{"value":{"entity-type":"item","numeric-id":1799120,"id":"Q1799120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$746381CA-621F-48B6-AFE1-FB78979AAD6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f681530f1e601559ae451198ac16d4e80569d32e","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$E2425720-2956-4266-8230-30BD459A50DA","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":"Q6844157$0ED8E1DC-C051-4713-A03F-5207FD2469D2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$8EA33B5E-5DB6-4076-B283-124218EBD9BD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cce7dbbed941893e1d4d53fc06f1e9c40cece671","datavalue":{"value":{"time":"+2026-03-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6844157$AB1D021F-279F-4166-9893-1314008FB2D0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6844157$0F109C83-52B6-4C27-8777-20806B452A5D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2666e454ff7116e808df1d61b7c61a4d0ae210af","datavalue":{"value":"8172633","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6844157$02E24397-2FFA-4AD2-9A27-38195D16D19B","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":"Q6844157$20C96ABE-A964-43D6-B416-69B6FA32A880","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"494aa31720bff090f87eabeb86ce7380ba058cbf","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$EDE00DDE-E9E4-46DB-9574-408CD28B57BA","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":"Q6844157$A89A02B1-2BC7-457F-8738-7D59DF51F9F9","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":"Q6844157$4C93D714-5D33-4F8E-9ECA-3076633B9F2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8bbbd10679bf2d321eb9db870479cc35412cbd39","datavalue":{"value":{"entity-type":"item","numeric-id":2104495,"id":"Q2104495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$50673836-06D7-4048-8C20-D0F318D0F24E","rank":"normal"},{"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":"Q6844157$B780C665-3DA9-42E6-90C2-F74CB29F0919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ead9660cd33cf6b597620bdfac44264e0480c8c3","datavalue":{"value":{"entity-type":"item","numeric-id":4647839,"id":"Q4647839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$7B1BE7FF-EDB3-4050-B602-FB83A45E88CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3fea6dff3d36407dad60fa8e8c9bcc1f06ec22da","datavalue":{"value":{"entity-type":"item","numeric-id":5200019,"id":"Q5200019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$37B88ECB-A546-4503-982F-EBFBE3CCEF82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd3cb6b9019747c7bbfc2bed55b78e42a7665495","datavalue":{"value":{"entity-type":"item","numeric-id":1663240,"id":"Q1663240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$517E3B22-4A86-4003-81DE-C48BE2659693","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6788f8c83d5a5db6237942eed0df1dc9fb4fc24b","datavalue":{"value":{"entity-type":"item","numeric-id":5919479,"id":"Q5919479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$74A761DB-AA56-4AAE-B22C-0E756FF5ED8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$28A4DB71-E4F7-4C4B-B262-F9A2A3B83332","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":"Q6844157$94ACA6BC-3FAE-424F-8ECE-0A64E339555A","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":"Q6844157$64A7303F-4769-4124-836E-4FE08148CF35","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":"Q6844157$95B20269-E1CB-489C-9DF1-9E1FDA3F7689","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":"Q6844157$89F6F601-8D2C-4027-AF76-01D38DDA21D2","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":"Q6844157$E21FB9D5-5C96-42A4-B071-684808A63979","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":"Q6844157$8477C534-C424-4A46-A485-2D1EE81C8648","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0007f6e6ddb56daad1917f282410760fb5b79ae6","datavalue":{"value":{"entity-type":"item","numeric-id":2870135,"id":"Q2870135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$247FEE89-76FB-461D-8FAA-512463D0880C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dad2502fac00d4559d492b4cdf38889af0b4e8db","datavalue":{"value":{"entity-type":"item","numeric-id":2891459,"id":"Q2891459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$CCAB11F8-7FEA-43DA-B262-C72330C06797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"142f36174f50b1d0c17981c7c8128c519fa77cbd","datavalue":{"value":{"entity-type":"item","numeric-id":2473610,"id":"Q2473610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$40DE3B7C-A469-4C27-ACB0-C03DFEC38ACF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"94b08b653c8ec14d2827bf7f8ead9e9fdac9c6b3","datavalue":{"value":{"entity-type":"item","numeric-id":6852300,"id":"Q6852300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6844157$35814943-5843-4562-9F69-8DC0EA2D8310","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":"Q6844157$B27FF3CC-B576-4E5D-ADD3-A102EB2ED210","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Reconstruction of SMT proofs with Lambdapi","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Reconstruction_of_SMT_proofs_with_Lambdapi"}}}}}