{"entities":{"Q5200015":{"pageid":7229586,"ns":120,"title":"Item:Q5200015","lastrevid":51306812,"modified":"2026-01-17T16:51:47Z","type":"item","id":"Q5200015","labels":{"en":{"language":"en","value":"The Matita interactive theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5934342"}},"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":"Q5200015$78C527D9-F3AB-40DA-8698-856B2941AB78","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8bfb0749a866724fb875d4dc50e330a9a70d56a3","datavalue":{"value":{"text":"The Matita Interactive Theorem Prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5200015$66114501-4E56-404F-A97A-8C9395084763","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5582423c4d0f78d4202eb93d4c429ada28480419","datavalue":{"value":"1341.68179","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5200015$E8C0D639-8896-4914-8CC1-1199C208D7D3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fbbccbb257bceb618c8e38a9ce56df284741a1c4","datavalue":{"value":"10.1007/978-3-642-22438-6_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5200015$0E40F7ED-38E0-43BD-BA91-4BD416B57780","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b7eb816b28b9c1f72e9b0af72e4651889c7844f4","datavalue":{"value":{"entity-type":"item","numeric-id":287278,"id":"Q287278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$C708A2E7-F59B-447C-8769-60B5A2DC31AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aec9839e6b2c451febe526ce547ea5fd11508ee1","datavalue":{"value":{"entity-type":"item","numeric-id":744985,"id":"Q744985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$B9C6901B-6AD3-4F0D-9BA2-1A85612409BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6fcc0863f3310792433a26fbf0220fe6380173d","datavalue":{"value":{"entity-type":"item","numeric-id":651318,"id":"Q651318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$F43327C7-CE31-4CED-A802-2088FE75D25D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"99729ea5fbac2e397c47743039765083a0ae1bb2","datavalue":{"value":{"entity-type":"item","numeric-id":205581,"id":"Q205581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$4A2A7D16-0204-41C0-803A-01C62A6153C2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$AEE39A43-F215-4349-873E-F3C655F82477","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d00523700407e21ae71debe0fbbbb012ba59e567","datavalue":{"value":{"time":"+2011-07-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5200015$5AA4AB30-A70A-4B0D-A303-9A6BDBEA9E29","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"07a9c92192bf4c6f5f9ce28cbf41803c805e58a1","datavalue":{"value":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.232.3171","type":"string"},"datatype":"url"},"type":"statement","id":"Q5200015$4A8E1779-A98D-4FF8-B919-B318B8A898F2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5200015$03221781-E41B-4B89-9354-EE835469261C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f1c004a9cd6c337626d04f3a76ebb2d5e6fb85a7","datavalue":{"value":"5934342","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5200015$B01430E2-7FF7-47DB-8EF0-FB6E056E7A56","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$510440CF-CE6B-4C18-8353-E247BEE3F1E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$D3DE8324-3052-4052-8E2A-1AEFDB32115F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6eebe30b9df25d8c347930b235e09f446ddc2fb1","datavalue":{"value":{"entity-type":"item","numeric-id":44157,"id":"Q44157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$28AACF4F-F87D-40AF-8B36-6861B85EFDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$A3EDA2F7-5554-4E32-BF3A-59EC29D30D53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$C2BFD58F-E72E-48EE-AB91-45CD7A10406F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8be5ee5254d2a781e0ec7bc0b35265c3f1813a9a","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$894919B5-F905-437A-905D-E062CDD1F116","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$AC8FD39C-B0E0-4666-9735-D607E2AB3330","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"83e2dec25ea583652d0e07d4393a843812f4b48b","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$168B7451-9F5E-4C2A-8382-1BBB76BEBFF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4f4a7d8a07c40281293b20fef0aadcbf0de2bbd2","datavalue":{"value":{"entity-type":"item","numeric-id":21949,"id":"Q21949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$38BE4B52-B410-453B-B352-672176E13D80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$ADAF1C5C-1FD9-4DB6-B4CB-91EA0DBECF68","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":"Q5200015$C8F9BE96-B6B0-4ABA-8F08-42753250D6F0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a120d616d05afc19b46ca9e8b7bde3ae499779bf","datavalue":{"value":"W2166662837","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5200015$09B840EA-0391-420A-BE75-6B66E10AB6CA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"cee68e943f423c6598b22e9df8e1ff7f83d287b8","datavalue":{"value":{"entity-type":"item","numeric-id":3497621,"id":"Q3497621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$E4E4991D-AB80-4604-A965-7291DE0BF296","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34babec465921f60dcf35356976f5e24742b5ce1","datavalue":{"value":{"entity-type":"item","numeric-id":5898170,"id":"Q5898170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$D19CCCC0-9404-4FC5-8C04-7F455DA171DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8635671f40deea656fb3b0cdc4e932d89e63f6b0","datavalue":{"value":{"entity-type":"item","numeric-id":3638243,"id":"Q3638243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$A4BBB05C-07C4-4EA1-8943-BC0D05A4E550","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5f64d57050206512889a218305d67a8f65e3f09","datavalue":{"value":{"entity-type":"item","numeric-id":3183522,"id":"Q3183522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$C15131AE-980E-4552-B9CF-CD602FE760F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c8847fc96bd6cc15667c599e80d53cc2bce3050","datavalue":{"value":{"entity-type":"item","numeric-id":2462635,"id":"Q2462635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$569CE419-C349-4575-8C09-4C0BC429425B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6f0974f54a711565a4787629b7615a083e221ca","datavalue":{"value":{"entity-type":"item","numeric-id":5166499,"id":"Q5166499"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$A1C855AC-2843-4F0A-BA36-F7FB1D1A1405","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"790431959cbc450f8f91911b56400214886e60fe","datavalue":{"value":{"entity-type":"item","numeric-id":3582713,"id":"Q3582713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$AE79715B-62AE-4AF9-912B-27477BDCD2BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1196f5e17dff99bc1a9d16ec3c58ef966832597d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$30C9FEAE-0361-4327-A2CD-D49C1730060A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79ce8544fc5a0489695eae9a558cb4d34b573281","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$60CACF28-4910-4783-A8C0-08C6D62236A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9225e2ac5be7718460c88d366c1fca51dbe066d","datavalue":{"value":{"entity-type":"item","numeric-id":2655330,"id":"Q2655330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$C7D058F6-B074-41AA-B032-99D4D73ACCE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33890b7faad584193275d91a4cd4d3b147aff5a7","datavalue":{"value":{"entity-type":"item","numeric-id":3541709,"id":"Q3541709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$481782A0-9409-428D-8BFC-77230803370E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3bbf5c4acba1e943106282227d496dff22117d6","datavalue":{"value":{"entity-type":"item","numeric-id":4238487,"id":"Q4238487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$EB2FF8CC-EC0A-4295-BEB4-C1F05B760782","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c00ecccc176b971f8f655f17f279ab75b6423f0b","datavalue":{"value":{"entity-type":"item","numeric-id":2432769,"id":"Q2432769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$AB606D90-3C39-4F3E-825E-58D04102C19D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30e65c74afe2b4d2d82d56db1a3dce7bdb46bda6","datavalue":{"value":{"entity-type":"item","numeric-id":3497625,"id":"Q3497625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$8D827804-CF79-4DCD-8DD2-6C38D23C166A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29209482615350601b1ac00dbba8b8d6f75d6148","datavalue":{"value":{"entity-type":"item","numeric-id":3499757,"id":"Q3499757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$C11A4291-12BF-470B-901A-4993F8C804E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0ecba633e7dd0ac407826dd5f559a4e819c3c8a","datavalue":{"value":{"entity-type":"item","numeric-id":2867943,"id":"Q2867943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$7B5C6356-CB34-4271-9D4F-608BECF1AE46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a55113899cd4fac58a731fff06a3c13ca370d426","datavalue":{"value":{"entity-type":"item","numeric-id":5313073,"id":"Q5313073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$129AFE02-F074-4DE2-8ABB-43C3C3AED412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ba8bd57f8794d317056b114a38bf751913f81c7","datavalue":{"value":{"entity-type":"item","numeric-id":3612448,"id":"Q3612448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$D9E4565A-3EFA-453F-BC2B-09501465E77D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ff7181965704e473c064c7d95f9f7f0b397f93f","datavalue":{"value":{"entity-type":"item","numeric-id":3543665,"id":"Q3543665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$3D309307-A683-4358-A878-7CD0B10F3FD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c66f03ae58a1984709b26c2c3abbc1577f8d3a6","datavalue":{"value":{"entity-type":"item","numeric-id":3561621,"id":"Q3561621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5200015$6BD9F228-F340-407C-9B0D-CB6E23079168","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af47caf822b03a03a704ed7ee8caa15dc6e408e7","datavalue":{"value":{"entity-type":"item","numeric-id":2462635,"id":"Q2462635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a269ca73fe4cf80b4054e01c724924778b15dff","datavalue":{"value":{"amount":"+0.8081241846084595","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":"Q5200015$60932FDD-EADA-4028-843B-C936EA6922CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de5b314669e1ea2254db5f3a4cdcc7d0c9f1cf1c","datavalue":{"value":{"entity-type":"item","numeric-id":5200125,"id":"Q5200125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff0f65ec383d5e08d321924b8525ec12c59e5b59","datavalue":{"value":{"amount":"+0.7998251914978027","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":"Q5200015$57B4BD06-172C-4C1E-9E3B-DE0A7ECB5AFA","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":"f970da4c9c0cb0a37fbf238916f5849c8647ed27","datavalue":{"value":{"amount":"+0.7984342575073242","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":"Q5200015$85B228D9-283C-464F-9FA5-9FD5942DD88A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38e415598554742df8b597e0c7f30c25756f3423","datavalue":{"value":{"entity-type":"item","numeric-id":3637307,"id":"Q3637307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb9d16c582803a3807894f274ab311c39b78030e","datavalue":{"value":{"amount":"+0.7867335081100464","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":"Q5200015$0C928CEE-09D5-4ED7-AE94-FD46C4A4DB05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2830883c821c59e8ea357fc4abf509bdbccc9c9e","datavalue":{"value":{"entity-type":"item","numeric-id":1945919,"id":"Q1945919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59233e3bb03f96610d90b31196980cac6eb4fd9d","datavalue":{"value":{"amount":"+0.7690594792366028","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":"Q5200015$5032F33A-D2EB-4543-B85E-E851EE5A01A1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5200015","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5200015"}}}}}