{"entities":{"Q1663212":{"pageid":1673953,"ns":120,"title":"Item:Q1663212","lastrevid":43268962,"modified":"2025-07-23T07:49:40Z","type":"item","id":"Q1663212","labels":{"en":{"language":"en","value":"Introduction to ``Milestones in interactive theorem proving''"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6921410"}},"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":"Q1663212$622E3CE5-ACBA-4BF6-A17D-148002CC8EF1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"405f3bf2ebe67eb1e187c350cd0f23473d155878","datavalue":{"value":{"text":"Introduction to ``Milestones in interactive theorem proving''","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1663212$79017508-405E-4331-BAEB-DE6DB7743DC1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3cba062f10f5a388f82cd8348e19b06d6453ab41","datavalue":{"value":"1398.00118","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$512BE68F-280B-4109-BB45-398821F59D23","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$159F443F-5A14-479D-A6E3-9BE8655D9BA7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1dea8b353f71cbbb3b5cacc724847e34eb1031d7","datavalue":{"value":{"time":"+2018-08-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1663212$5D954E71-2F14-4B28-B6A1-E2D50AB76EFA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7f3250f85a60520aa08200c2217f8a3a516162f6","datavalue":{"value":"https://research.vu.nl/ws/files/118674118/Avigad2018_IntroductionToMilestonesInInteractiveTheoremProving.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1663212$C5BF2B7F-1D26-4F03-BC13-D11B07CE2C6C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"621c5eb61e35215bb5d90ba240e258b1da91aac9","datavalue":{"value":"00B30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$249033A4-C28B-4C62-B95A-EAC78304BBF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$4ACC77DD-25B4-4A6B-9B62-4F2B53084563","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$49E16E59-E4E7-4D44-97B5-66BB8C6D2870","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"dafba5f17d257d46259dc5c8486d872524e357b4","datavalue":{"value":"6921410","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$39B9CA5F-FE58-44B4-87A2-9984C0BDC186","rank":"normal"}],"P1463":[{"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":"Q1663212$18D8B6FB-FA7A-4821-AE7F-A217225DCEFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0aae91b3cebe1e84c9813205ff5ebc7d8b0f6804","datavalue":{"value":{"entity-type":"item","numeric-id":18521,"id":"Q18521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$82A726A4-7996-4C9C-86F4-18AC235122EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f3dc49212bb1ac953b456b7ee6d37c17258b97b9","datavalue":{"value":{"entity-type":"item","numeric-id":18543,"id":"Q18543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$041415A2-BDDF-4B3E-9B0C-A7FBA2237A3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"66eb045e037081b6f6e8499f9fef44d8fbb7e0b0","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$3CCBEB49-8B9F-430B-A9EB-8F9BB1361979","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ecb36fec89ff827cd73a8ca1a85f36a2e419c34e","datavalue":{"value":{"entity-type":"item","numeric-id":13377,"id":"Q13377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$2BD5334B-B7EC-42F0-A24A-AAD4B7A9EFC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$EEB23D3D-E453-4128-B37B-1911409F7114","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e0a25f11521438371c8e6ad465b53d2cb40829a8","datavalue":{"value":{"entity-type":"item","numeric-id":40292,"id":"Q40292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$D0CA122B-9EF8-41DE-84CC-E9A52FFFD950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$55124F83-3182-4855-A487-BC60BB1CFB5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2ad21f150c621099eebc7c2e673cd9cf43b81a4e","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$95046CAE-35FD-415C-A3D9-39F9A342DADA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$4A8D274D-6DD3-4DA8-A02D-2184F33D39E4","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":"Q1663212$70EACE13-4C3F-4349-A680-35028D6E881F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aee73c8b388d432beaaeff6eeea009516921e6ed","datavalue":{"value":"W2801537935","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$AC896A50-D90C-4288-8912-97C2D3AED36A","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"feaa63142ef8af21998480d463ce2649eb428b40","datavalue":{"value":"Q57382527","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$FEF83003-27DB-45F7-AB26-8B87DA094321","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"25aace5bdaaa9fb0a7bec1534f06ed96f3ade7f9","datavalue":{"value":{"entity-type":"item","numeric-id":947830,"id":"Q947830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$FA23DB0B-86AE-4E8D-ABFC-4977AF804EE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$40DBEA3B-A491-4E59-80AC-A40E41B88010","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":"Q1663212$13E94A7D-233B-4D2A-8A7E-F96403D1F03A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c60f93a1843fcd9c0656971efa4327b435decb9","datavalue":{"value":{"entity-type":"item","numeric-id":4736387,"id":"Q4736387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$4B4B256E-2CE5-4388-B708-75293863533C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49023bd5aa461c9f63f0725228815aa2af2e478f","datavalue":{"value":{"entity-type":"item","numeric-id":5747646,"id":"Q5747646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$D4D9BA6E-0947-4533-867E-869D0CC2DAC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c39b9040e3d2807bc13175b6074f0175a0a4a1c","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$0A4E20D3-2D17-4C79-8983-E771E2534DCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78757e9c4e37a9fa53a10705a27e9c8cff416b63","datavalue":{"value":{"entity-type":"item","numeric-id":2324018,"id":"Q2324018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$34AFC0A2-1872-4DC0-B89E-8099E3B3BC69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bf52ff9535def97a60a78e4a20f91c32385652c","datavalue":{"value":{"entity-type":"item","numeric-id":1112626,"id":"Q1112626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$2A2967D0-6E8C-4D7D-8607-A5471BCF9D32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"871979c7f5f894fa361fd2bc427b689835df215d","datavalue":{"value":{"entity-type":"item","numeric-id":1824411,"id":"Q1824411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$A73B215C-9CC7-47F0-BDF2-1403CC92E0D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4e12a81eacd6b45bc4b4689eee451512cadf31d","datavalue":{"value":{"entity-type":"item","numeric-id":3985547,"id":"Q3985547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$5FC8E276-D0E4-4A0E-B7D0-CEA5447ECB92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5809a6684c365442525c649f10f3cfd46627fcb","datavalue":{"value":{"entity-type":"item","numeric-id":1825045,"id":"Q1825045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$0EA9F550-6625-4809-951A-ED9AD6D479F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d120742af8436a54e9c640ab06706d350dfdb2b6","datavalue":{"value":{"entity-type":"item","numeric-id":909488,"id":"Q909488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$8C0FF874-15E6-4B65-A27B-492F5617AACD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ac14b4a963fe8ffd6a9a7c2d0ec85f99c6c6cbb","datavalue":{"value":{"entity-type":"item","numeric-id":3495674,"id":"Q3495674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$C6D76038-41BA-4E29-BA79-8A7146DACA34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a6b1d15dbc2412bd2d097ea4c4b2ce5e2ecdcac","datavalue":{"value":{"entity-type":"item","numeric-id":5881304,"id":"Q5881304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$FAC4EF3B-EC6A-42FA-9762-F7D2C3C43909","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da6449fa32317f64e0e88162e1e76272b77ced27","datavalue":{"value":{"entity-type":"item","numeric-id":1272764,"id":"Q1272764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$21AE87CA-15C2-4676-99C8-268B2A565870","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59d689c6ebe5f4ce66342ea706faf5cd9a7eae98","datavalue":{"value":{"entity-type":"item","numeric-id":2769440,"id":"Q2769440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$504A9F65-6188-4DE7-BEDE-6F2437A0A3AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8219577a178b5e6bc0cc5aede73996c94784449","datavalue":{"value":{"entity-type":"item","numeric-id":4435474,"id":"Q4435474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$6C2B3029-7077-4D78-B729-07158BB7700D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836a1d7b6bdb48a4904f72118ea93610f12fe959","datavalue":{"value":{"entity-type":"item","numeric-id":707743,"id":"Q707743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$5044A6B5-7914-41D6-AADD-267AEDF70D38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19187356da9a378282bb90537d8cca82d9231e95","datavalue":{"value":{"entity-type":"item","numeric-id":3613398,"id":"Q3613398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$4D6AC362-A883-46E1-9DB0-EAA0E21DC0CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e264974062f53b439460b85662778a60b49509d","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$BE7AB346-4B5D-4222-B4A3-8C5DE314E5EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"96b72cabd2b74d40b17052d73f277b61c8ea7e0f","datavalue":{"value":{"entity-type":"item","numeric-id":5055760,"id":"Q5055760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$211044D7-07BD-4962-92DF-306473A8CB39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"136dca5eaf30010d2d4c0f6c9100d687138b0eac","datavalue":{"value":{"entity-type":"item","numeric-id":3956381,"id":"Q3956381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$6B3B0B82-19E9-40C1-B16A-CD22CBD34982","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ec976db9fee9bededf233dd7d31c7e9ef2213c8","datavalue":{"value":{"entity-type":"item","numeric-id":5705937,"id":"Q5705937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$AFC8E2A0-CF4B-4879-97F5-AE3065E4F428","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb636a19f07738495cd7c2789db1b47cb8caa811","datavalue":{"value":{"entity-type":"item","numeric-id":4329634,"id":"Q4329634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$7C6C9556-481C-4710-8106-87DE86BC40FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f77ae6eb05f558a0d227a41ff0e65678671b287f","datavalue":{"value":{"entity-type":"item","numeric-id":592091,"id":"Q592091"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1663212$8623B979-A7FD-4A64-9B0E-A6B95D26882E","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"8ae566d0ab905ee24865a78bd72894f4c4b560a9","datavalue":{"value":"journals/jar/AvigadBKPPS18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$10B4C133-706C-41D2-BB0C-D6A5C03B46FF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"63d02a56309098235000f33bd10aafc8cd7d5886","datavalue":{"value":"10.1007/S10817-018-9465-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1663212$4D975E62-5C8D-4E97-B0C4-D8AE7F2BB3EC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1663212","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1663212"}}}}}