{"entities":{"Q2117791":{"pageid":2128534,"ns":120,"title":"Item:Q2117791","lastrevid":43523462,"modified":"2025-08-18T07:52:32Z","type":"item","id":"Q2117791","labels":{"en":{"language":"en","value":"On preserving the computational content of mathematical proofs: toy examples for a formalising strategy"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7495176"}},"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":"Q2117791$FCEF76E5-A5DF-434D-ACF8-8585B053DA62","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a82578a2148fc5e1fc08c8454f7e0547b213bd8f","datavalue":{"value":{"text":"On preserving the computational content of mathematical proofs: toy examples for a formalising strategy","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2117791$853E909C-E53F-4339-84E5-315CF78382F0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a71d929176ba085c820b274734a7e59de6c86e08","datavalue":{"value":"10.1007/978-3-030-80049-9_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2117791$977A40F6-7B5D-4E42-BA38-5CD355A6D93C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"43720d5641a605df4a870ccd696a31d0b30078dc","datavalue":{"value":{"entity-type":"item","numeric-id":472315,"id":"Q472315"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$C9F48855-43A7-4E2C-A8A8-063D973E051F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"39b1515277af1c7c28c7fc6f6f97d2379899717d","datavalue":{"value":{"time":"+2022-03-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2117791$2244C037-1232-443A-BF71-AE2F884FDCE2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2117791$540C9B98-E2F4-492F-B4E5-B3170997090A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f29f7aca8fbfe4165e618a84f989281a386b6ca8","datavalue":{"value":"7495176","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2117791$E347960F-9EF5-43CD-8500-8BC460C28A96","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2117791$8F50E846-4BE5-436F-982E-2EE023735080","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78f7fac8324c6ac945fcbe3570af48d82a2920e1","datavalue":{"value":"computational content","type":"string"},"datatype":"string"},"type":"statement","id":"Q2117791$F2207F98-5838-4765-B121-12C65F693F44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7c23305d5a301c23057fddc53953635a4398a76","datavalue":{"value":"proof mining","type":"string"},"datatype":"string"},"type":"statement","id":"Q2117791$0FA9D692-4A5C-44D1-800D-B199939747DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2117791$A2F6C68F-067B-4B39-87EF-0C6577F6CFDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2117791$A1308979-42C2-4BFA-AF3F-13B32BE0589D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82db2410f7cb36b26154919ad626ca1e681d8b2b","datavalue":{"value":"interactive theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q2117791$E2916C41-4BF1-40B7-A698-68493D91A85F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"edc0dc7c05f75a6364f0dcd54ee6aed1a8932214","datavalue":{"value":"formalisation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2117791$41B44DFF-F7E7-402A-AB02-D14AA606E6E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2117791$FE2A08BD-4FAF-4A67-826F-B52B54CE37D8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$D26FA605-EDF9-415A-BB63-6709E8DEC6D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"efbc9c0ffecce111990689e7c9fa5153da65c282","datavalue":{"value":{"entity-type":"item","numeric-id":5972779,"id":"Q5972779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$135249EE-EBDB-4FCE-9AE9-74D392D1831F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$F68F682A-A286-482E-828F-A889EFEF706C","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":"Q2117791$B65D3242-5B51-49C5-8F61-91D020C44377","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"af8b574580d64576fe2e84cba54865ffcac7d01d","datavalue":{"value":"https://doi.org/10.1007/978-3-030-80049-9_26","type":"string"},"datatype":"url"},"type":"statement","id":"Q2117791$7D0C0789-B37F-40BC-A4B3-90733227837F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"850c82b0c0defd0bc1fee856482c05ec5fd89200","datavalue":{"value":"W3185513211","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2117791$C02544FC-B8A1-4141-B319-7877A595A9E8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ed1b13de1c0020bbe1572fd803af838cdf98974","datavalue":{"value":{"entity-type":"item","numeric-id":3001090,"id":"Q3001090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$B8397169-0744-4D7F-9F53-5F8A99DE7FF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00dc33dea4817e979298e9fc83730810ceee2e27","datavalue":{"value":{"entity-type":"item","numeric-id":4553308,"id":"Q4553308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$8BD158C8-5962-4413-A93E-153F97BE9973","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68c91066f858fa64a799af591825e0694228fffb","datavalue":{"value":{"entity-type":"item","numeric-id":4122841,"id":"Q4122841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$C44BD192-2E04-4D24-8276-5A6C3346DC05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494d4e4ed60b0c479ddcb5a7f505faa8dd66ad12","datavalue":{"value":{"entity-type":"item","numeric-id":5563103,"id":"Q5563103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$C5251701-FC39-41E3-A0E7-3472F431E12A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe7f73b08df7100728ceede07434a97e2ff97fd9","datavalue":{"value":{"entity-type":"item","numeric-id":4012886,"id":"Q4012886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$BC4C35DB-6AE4-463D-BC6E-6917C48673EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22be7e7575326e176489e7e8e8b0922b28875ea5","datavalue":{"value":{"entity-type":"item","numeric-id":688431,"id":"Q688431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$EACFDBFB-C974-40B3-91E9-DCBD703E6BD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e73cbdc4f532ed72bacdc9e85f4929b162897095","datavalue":{"value":{"entity-type":"item","numeric-id":5450521,"id":"Q5450521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$F405C595-897A-49CA-B04E-09F35E04C1D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c7b2ea62a61340c30ced0693795d31f5e2d749a","datavalue":{"value":{"entity-type":"item","numeric-id":5122020,"id":"Q5122020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$F698BB33-191B-4D59-9A91-3C454329085B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcbc165942591c59054a8d2cf0de0849a34e3863","datavalue":{"value":{"entity-type":"item","numeric-id":472316,"id":"Q472316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$A018C462-48ED-47CD-BD95-9A1F34FA2712","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"811e7c8176b4c38101368323673a203b61fa4952","datavalue":{"value":{"entity-type":"item","numeric-id":499259,"id":"Q499259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$4E3F1888-953A-4DD7-B400-A15487A78C77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66d4c354863112eab3a59c0306db41440d797bc8","datavalue":{"value":{"entity-type":"item","numeric-id":2657827,"id":"Q2657827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$9FFCA740-9197-4176-A88A-B4FD34446F07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1bb6050f4b8cabf1a876b4ccd984e38edee73579","datavalue":{"value":{"entity-type":"item","numeric-id":4555782,"id":"Q4555782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$75B3A54F-CE38-4663-9DBE-E010495BD0AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24ee03de20d1d8956ad0cb418b2df29314faf41c","datavalue":{"value":{"entity-type":"item","numeric-id":4602172,"id":"Q4602172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$8047E3D4-93FC-4E7A-89D3-E2304CDA4C81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fedc989743450d73f97e8776a70bc3acbadc173a","datavalue":{"value":{"entity-type":"item","numeric-id":5272532,"id":"Q5272532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$5D56CBAE-1E69-4EFA-B641-E9CBE7A39AA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d966d8fb41a3564f4060a1b833eb768ac2e0597d","datavalue":{"value":{"entity-type":"item","numeric-id":5806808,"id":"Q5806808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$2B4F23A8-E75B-437C-B9B4-FCC4F5543143","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98a0f5ab3a82f792e215192b74a3f7485b0840ad","datavalue":{"value":{"entity-type":"item","numeric-id":5809142,"id":"Q5809142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$6E11A55C-4B98-43B8-B070-E4ED5D82FFBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ac3bd59819bab3c20ab46afa2f257091fcd8fbd","datavalue":{"value":{"entity-type":"item","numeric-id":5344164,"id":"Q5344164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$1DFEE765-95F4-4043-B01E-D88FAFA1D7FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"334057c9297d6a0878784b79f130fef6a1b466a8","datavalue":{"value":{"entity-type":"item","numeric-id":3110202,"id":"Q3110202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$C6C24EF1-6E31-406B-9C0B-6043882E8D57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad4168c7403b3e6139601a0e087b810e4ec38e2d","datavalue":{"value":{"entity-type":"item","numeric-id":4989411,"id":"Q4989411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2117791$AFBF1499-4FE7-401E-8C12-DC7451CC336D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2117791","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2117791"}}}}}