{"entities":{"Q6496633":{"pageid":14075406,"ns":120,"title":"Item:Q6496633","lastrevid":103419416,"modified":"2026-06-06T07:20:12Z","type":"item","id":"Q6496633","labels":{"en":{"language":"en","value":"Learning Proof Transformations and\u00a0Its Applications in\u00a0Interactive Theorem Proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7842302"}},"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":"Q6496633$14EDEB87-49F4-4BAC-8A2E-918A90C367C7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"390fb1c173a52fc94db5b1333393ca823685c7d6","datavalue":{"value":{"text":"Learning Proof Transformations and\u00a0Its Applications in\u00a0Interactive Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6496633$DAAAE1EC-1D87-4F7F-A8AF-4F1AADC1B720","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"96b4c1b9087918f8e86c26cf5fd48fa5a95daccc","datavalue":{"value":"10.1007/978-3-031-43369-6_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6496633$31F0B62A-BEA4-4E6C-9914-0CEB7936FAD6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d60f422ea4078f78ffdc41c4f2ebf2d1fdd669e","datavalue":{"value":{"entity-type":"item","numeric-id":2128794,"id":"Q2128794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$DF78C25C-BED7-4F79-B96B-73D8203BEBF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a2a10f8493b6d512bfd4eade8423906525f6e138","datavalue":{"value":{"entity-type":"item","numeric-id":2128795,"id":"Q2128795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$1BA334B9-440E-4475-9EAF-5814BDC44DAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$E9964BBE-89E3-432D-9422-A3634CB47D2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$04A12F7F-541A-4024-9523-6411B9C13434","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cfe8f812c44973320a5b5393ac1a99b462a2ece6","datavalue":{"value":{"time":"+2024-05-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6496633$2843A770-7C5C-47FE-9E4B-D4DB09DA3474","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"18309be7db1da1fcc09fdceba48f604c7de62db3","datavalue":{"value":"68Txx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6496633$2999B550-A231-4930-9CEF-CF8DBA375C22","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0cb22a7dc4152f2cf8813307a0fc66e900728421","datavalue":{"value":"7842302","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6496633$6A91EECD-B649-44F0-92CA-F56E267F28AA","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":"Q6496633$01C59B07-A1A1-4548-896B-61CC824FF618","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"29b0802dd9ffb89108bee25aa26120dffc46ad60","datavalue":{"value":{"entity-type":"item","numeric-id":2352489,"id":"Q2352489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$8A263CD4-EE4D-435B-BBC7-BA4C0288916C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ebbe3f6a88e51e1203c3c8190dcfbdac3cc8dde","datavalue":{"value":{"entity-type":"item","numeric-id":1663215,"id":"Q1663215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$25E95818-358D-4E03-96BB-C910143FF9D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5552c73af9ffa4d08773105bfa675feb6642eb2e","datavalue":{"value":{"entity-type":"item","numeric-id":3453119,"id":"Q3453119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$4293F5FD-4556-4B0D-BF80-E65B28AEFC4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3af6b847528569308c270822a9e669d3f5e692fc","datavalue":{"value":{"entity-type":"item","numeric-id":2219409,"id":"Q2219409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$A33DFCDE-D56F-405A-BF5A-6448943A376C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a73b7e48adb4260cb48d91e95198beb0803e94","datavalue":{"value":{"entity-type":"item","numeric-id":5952197,"id":"Q5952197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$A3F29935-785B-433F-9EAF-1773C184F5BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4333233391b31141e0029e0c5598f36189360b55","datavalue":{"value":{"entity-type":"item","numeric-id":2817934,"id":"Q2817934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$0439E4B3-A1D8-4CE1-BC01-8C471E099BCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be2e8f4770b19dfe4ed5db70d9e22ebf6c799bda","datavalue":{"value":{"entity-type":"item","numeric-id":1640642,"id":"Q1640642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$6FEA0B06-C9CF-4C00-A32C-032D586EF6FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c577e428611609f51c98d78844448d28a70865f","datavalue":{"value":{"entity-type":"item","numeric-id":2031416,"id":"Q2031416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$E6762C96-8A2F-4F40-80ED-3535BCB655EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da7d80b034d5bbc9c7be0be22781c5c67e99e185","datavalue":{"value":{"entity-type":"item","numeric-id":3454097,"id":"Q3454097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$510F7187-0F14-4213-A404-CBD0531391AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0478213a2768e15885bd259a974294cbcf32b5e0","datavalue":{"value":{"entity-type":"item","numeric-id":4619818,"id":"Q4619818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$68DBD2A1-8D88-4505-A1C8-752EDCD30E73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e74d3fce405174a77b93de2a6b609361e3b5e6c0","datavalue":{"value":{"entity-type":"item","numeric-id":2364687,"id":"Q2364687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$764E46CD-269A-4DCD-A54C-33AE52C042D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdaf319ddaeb6a52a60a91025cb24f95d8069611","datavalue":{"value":{"entity-type":"item","numeric-id":1687711,"id":"Q1687711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$8200B9B9-B7E5-448B-861A-3E7568305878","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb40d55c384e43c0f7f459b4c221814c7ba3e671","datavalue":{"value":{"entity-type":"item","numeric-id":4398828,"id":"Q4398828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$09DD3FBC-3374-429E-8DDD-DDFFBA070478","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$88C158DB-D926-48B9-B089-2973F4BB6729","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b5e4c8820eb3333a06a963b91456bb31fc1405c","datavalue":{"value":{"entity-type":"item","numeric-id":5219927,"id":"Q5219927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$E1542E99-4FE2-456C-ACFC-E00BA9A005A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea3dda75970a4bd0a41ac690f289b5e07ae9c635","datavalue":{"value":{"entity-type":"item","numeric-id":5677085,"id":"Q5677085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$55E09007-56C0-41F1-BD19-43658FB61457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3d307a31d75ce205d43f99746df1f049e810792","datavalue":{"value":{"entity-type":"item","numeric-id":5624680,"id":"Q5624680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$AE43C2A0-75A4-49A9-8DBB-AC15040805C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$D6272FB4-85CF-4F3E-A832-9F1427C6E68E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5402ee74270ab8c51652a1b8671f28fcac792662","datavalue":{"value":{"entity-type":"item","numeric-id":831938,"id":"Q831938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$F49056AA-C0C2-4107-92E5-C9C1E375D902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a3c272427435848e695b99f7aab5900f31907e54","datavalue":{"value":{"entity-type":"item","numeric-id":2219416,"id":"Q2219416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$C07121DA-D94B-4774-9EB2-38690151BEE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4a29860ebd84f7337a18d8f88370124a69396a2","datavalue":{"value":{"entity-type":"item","numeric-id":2128797,"id":"Q2128797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6496633$7CDE3FD9-2456-4B4F-ADD0-F6A4B6BF317F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"769132f455520660740ddeaf8b17556763746c2e","datavalue":{"value":{"entity-type":"item","numeric-id":2031416,"id":"Q2031416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d9bb0bddab8113b246889b0c572f2ec1f2dcba4","datavalue":{"value":{"amount":"+0.7992661595344543","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":"Q6496633$7C4E27EA-DA0D-49D2-A0C2-B0E83965E2A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68b122fc17cf6c180e33e2295f43b455fdd3224f","datavalue":{"value":{"entity-type":"item","numeric-id":2219409,"id":"Q2219409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46c5bee3cc336cbba49e5fd008f23a7a528e78f7","datavalue":{"value":{"amount":"+0.794077455997467","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":"Q6496633$7D416D32-1613-4CE2-A36D-CE3768C02F15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80a02b86f5e7c12a000ea62837c3061ae5ebea26","datavalue":{"value":{"entity-type":"item","numeric-id":4645730,"id":"Q4645730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c31186c3816c09bd6df20bd795b68cc642cd1f54","datavalue":{"value":{"amount":"+0.7874382734298706","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":"Q6496633$C5B661EA-A7A3-4228-892B-9BABCA011C67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"196c6be9bd3eff3fdeb14496a3810135fab697d6","datavalue":{"value":{"entity-type":"item","numeric-id":6118837,"id":"Q6118837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07bfdab6c1452379590ee0d6d42842b0547e34a0","datavalue":{"value":{"amount":"+0.7628805637359619","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":"Q6496633$AA8CE11D-00E8-4A16-BA42-E85CF96492E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"733045d4bdb6ac84e39d437da15db86acd1c641d","datavalue":{"value":{"entity-type":"item","numeric-id":6108816,"id":"Q6108816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e599c20cf21c728dae5a2b5979bfed9ae067e4a","datavalue":{"value":{"amount":"+0.7392761707305908","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":"Q6496633$AD37210F-A431-43C1-ADA3-1DDE70AFE36B","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":"Q6496633$FF5EA0C7-62F6-484A-8CFF-D75BA5CF6376","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Learning Proof Transformations and Its Applications in Interactive Theorem Proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Learning_Proof_Transformations_and_Its_Applications_in_Interactive_Theorem_Proving"}}}}}