{"entities":{"Q7361207":{"pageid":31519160,"ns":120,"title":"Item:Q7361207","lastrevid":105363953,"modified":"2026-10-07T13:35:13Z","type":"item","id":"Q7361207","labels":{"en":{"language":"en","value":"Extension of Types-To-Sets"}},"descriptions":{"en":{"language":"en","value":"AFP entry Types_To_Sets_Extension"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fe58f1a7c33ba9f640c441d2a3ccf144c9003428","datavalue":{"value":"https://isa-afp.org/entries/Types_To_Sets_Extension.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361207$C23D1BC1-360C-4FE7-8AA1-ABD0476055D5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"18957d200fe2c6707b918f1bb8bf691a5624f8d8","datavalue":{"value":{"time":"+2021-09-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361207$855F49A7-CB8C-4D88-BF0D-8AFDC4AB017E","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"a738e4c63b1e8a2b5c81f7e7de071e7ee4c81712","datavalue":{"value":"Mihails Milehins","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361207$F6285B5F-E834-4583-B13B-E32DA397218F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"864b2cc11c3875bdb8f00e0f5fa09c6ebd750f5d","datavalue":{"value":{"text":"Extension of Types-To-Sets","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361207$9573572D-35B4-456A-B91B-B898893121ED","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"23841689aa624de4a53b1ad9148875de221d7a02","datavalue":{"value":"In their article titled From Types to Sets by Local Type Definitions in Higher-Order Logic and published in the proceedings of the conference Interactive Theorem Proving in 2016, Ond\u0159ej Kun\u010dar and Andrei Popescu propose an extension of the logic Isabelle/HOL and an associated algorithm for the relativization of the type-based theorems to more flexible set-based theorems , collectively referred to as Types-To-Sets . One of the aims of their work was to open an opportunity for the development of a software tool for applied relativization in the implementation of the logic Isabelle/HOL of the proof assistant Isabelle. In this article, we provide a prototype of a software framework for the interactive automated relativization of theorems in Isabelle/HOL, developed as an extension of the proof language Isabelle/Isar. The software framework incorporates the implementation of the proposed extension of the logic, and builds upon some of the ideas for further work expressed in the original article on Types-To-Sets by Ond\u0159ej Kun\u010dar and Andrei Popescu and the subsequent article Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL that was written by Fabian Immler and Bohua Zhan and published in the proceedings of the International Conference on Certified Programs and Proofs in 2019.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361207$6E3B08C4-3DED-43A2-87D6-1C05E7DBCF07","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"14533123e0b9e73c06f9737a070ee002c25f5f1b","datavalue":{"value":{"entity-type":"item","numeric-id":3612442,"id":"Q3612442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$EF3957B1-B7C9-4EC2-B075-F9511A198AFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$1A7BA8D9-88A8-46E5-93D4-4194B184D405","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a655377852f4fbc1e40cdceec18686655bda680","datavalue":{"value":{"entity-type":"item","numeric-id":5712320,"id":"Q5712320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$6A01D2D9-1BC4-4D27-AEFC-4BD0BDD0D1DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a5cab1513e2457c77b799379237c33e5461fd89","datavalue":{"value":{"entity-type":"item","numeric-id":2829259,"id":"Q2829259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$4A035B75-7607-436E-8659-B860509D63DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$2B22B861-71F6-4882-B8CE-024F125803CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54eee2313932f532ca016c516cb047dfc95351e0","datavalue":{"value":{"entity-type":"item","numeric-id":5428257,"id":"Q5428257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$0C38B4F2-D27B-4677-8B18-CE6AA44CD445","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67c913a72527b57ea467866b24b8cfd23fe78226","datavalue":{"value":{"entity-type":"item","numeric-id":5747659,"id":"Q5747659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$C7E6CC55-21BF-4BFC-97BB-73E9CDE14B99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a1a0dcbfc561e1e5ffac774e9501a5c3c966797","datavalue":{"value":{"entity-type":"item","numeric-id":1722645,"id":"Q1722645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$5B598AF3-2AC2-4670-A652-052EF88BC8D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50b0bfaa5604fbbf1607bb7e54efdd2fee887b49","datavalue":{"value":{"entity-type":"item","numeric-id":5327338,"id":"Q5327338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$B4DAFA80-C16F-4AF6-8D79-6F44C3DD7597","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$EF0FEAE9-2A38-4F9E-BAA6-7737D24AE9F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab8d7dcc337f0f7083d889ef5fbd195dbcbfcdc2","datavalue":{"value":{"entity-type":"item","numeric-id":4720797,"id":"Q4720797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$4743DCEB-991F-4B1D-B999-A639235EF26D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e002a9754659cf7f51ada447f1ca688729d010d2","datavalue":{"value":{"entity-type":"item","numeric-id":2287890,"id":"Q2287890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$B3BA64E0-787C-46B2-9514-ED579D680B52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2622e8892c0aaf09e727281c5cb9109808708d59","datavalue":{"value":{"entity-type":"item","numeric-id":2988665,"id":"Q2988665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$27839365-9681-4EDA-B73D-A4EDDF86FDA0","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$68FAD7E4-C277-47B3-BDCB-D7BB47F29977","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"42b8213d2a1dfccb90d4e642f9815041158f508a","datavalue":{"value":{"entity-type":"item","numeric-id":7361814,"id":"Q7361814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$67DD0D16-AE99-45A6-8958-7AF6AE7C8FBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"35972e4d852b9a97437a6c555f7480f3e52c8876","datavalue":{"value":{"entity-type":"item","numeric-id":7361511,"id":"Q7361511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$BBA2CE45-318E-40BD-A5D0-22473B3B8098","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$4E53E34E-9232-4239-B36E-232410440E65","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361207$3E7FB8AA-EB6F-4A20-BC59-600667132CE0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extension of Types-To-Sets","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Extension_of_Types-To-Sets"}}}}}