{"entities":{"Q6173578":{"pageid":13308466,"ns":120,"title":"Item:Q6173578","lastrevid":102461996,"modified":"2026-06-06T04:31:10Z","type":"item","id":"Q6173578","labels":{"en":{"language":"en","value":"A survey of interactive theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7715474"}},"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":"Q6173578$03A97155-8655-47C6-8D8C-D6A89A6DE30F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"30659652a6bb6474380a07a770377c63fcc6c983","datavalue":{"value":{"entity-type":"item","numeric-id":606998,"id":"Q606998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6173578$74322409-376F-4098-8132-9083EDEDF69B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ca9f8142551b5159c71df5982bbefa0ef87fa1c3","datavalue":{"value":{"time":"+2023-07-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":"Q6173578$F6480F62-323E-412C-BBC7-8214F3C5D63F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a7f4cf38ad186857fffb43f92cc209dc9a61576b","datavalue":{"value":"http://elib.mi.sanu.ac.rs/files/journals/zr/26/zrn26p173-223.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q6173578$6FB2D532-B8C5-4805-B7DE-0D17EE8A891F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6173578$E766D06A-4F4A-452D-A500-99CA4F1626A0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5387be69d2797a2e82b42219f90f781aa31c56e0","datavalue":{"value":"7715474","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6173578$94C9B195-906D-423E-8C74-F31E923712A8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6173578$AD2025BE-7672-4378-8DE4-B01A87CFA235","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q6173578$16CC8066-F11A-4DCE-A702-2C4ABC601AFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd6f648bd1eeb66cc548d9608d64c3a3e1ea7e29","datavalue":{"value":"formal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6173578$EBA83564-43C1-4598-9539-D718B709FB25","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":"Q6173578$2F8A2523-83AF-4061-9BAB-EF2EF6EB4031","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a02b2bfea1c5f47cd601f5ce8d9525ee86d87fe","datavalue":{"value":{"entity-type":"item","numeric-id":5219926,"id":"Q5219926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"edf94e11ee24a1dd9db83a2708d9a407b89d339b","datavalue":{"value":{"amount":"+0.799427330493927","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":"Q6173578$177A923F-A7B8-4367-9CCC-B24B01595C6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3634c26162d01a1765d928ca49ece4b187f75c5f","datavalue":{"value":{"entity-type":"item","numeric-id":5166499,"id":"Q5166499"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"313281dbfa48941ad51b52ae54d8ccd81cce309f","datavalue":{"value":{"amount":"+0.7805835604667664","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":"Q6173578$A6D1C5FA-9260-452A-8F4D-D1321BC19E2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c32f2cbb8a453222b98cdf0e974734e0b4ea4a11","datavalue":{"value":{"entity-type":"item","numeric-id":5094469,"id":"Q5094469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c31351b5b68a555a44270a711bf9e03b21d18f58","datavalue":{"value":{"amount":"+0.7752888798713684","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":"Q6173578$1B67E632-07A7-424C-8BBF-BEE7ED6E537A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef987661b418b289e2924d474c61a925bb8556a0","datavalue":{"value":{"entity-type":"item","numeric-id":2843039,"id":"Q2843039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da10da0e091cf041f2364bc3dd0298dfc2dcab94","datavalue":{"value":{"amount":"+0.7730091214179993","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":"Q6173578$95A3A4C6-C1C9-4D6B-B8FF-3BC468E4FCB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdade178ac9ba6848e51f8546460e812ce1b68c5","datavalue":{"value":{"entity-type":"item","numeric-id":5200015,"id":"Q5200015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2eae2582cde4e15372d31d8db8944d52ac934ee","datavalue":{"value":{"amount":"+0.771900475025177","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":"Q6173578$ECCE1B65-4223-4683-80BA-2ED46A68E380","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A survey of interactive theorem proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_survey_of_interactive_theorem_proving"}}}}}