{"entities":{"Q1945919":{"pageid":1956661,"ns":120,"title":"Item:Q1945919","lastrevid":69831909,"modified":"2026-04-13T10:38:44Z","type":"item","id":"Q1945919","labels":{"en":{"language":"en","value":"Formal metatheory of programming languages in the Matita interactive theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6154940"}},"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":"Q1945919$D68F3071-7F2C-4438-9FA8-3E49F618A96B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8e05c2eadb0a06467a3dce8e2adec77a33a47bbf","datavalue":{"value":{"text":"Formal metatheory of programming languages in the Matita interactive theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1945919$196C29EE-0A42-48C9-A223-B677DA7AA536","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"14fb351fbc609d751b7071b1f0acc8dd153c0723","datavalue":{"value":"1260.68363","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945919$1F43E8A2-3EEF-4105-BC6C-31B2A0C0B203","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":"Q1945919$E3B45592-D2E8-42A9-B526-1F72BAC252F8","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":"Q1945919$14D38E54-8531-4F9D-B8B3-766BC019786F","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":"Q1945919$D9F2218D-B11B-4E80-A68E-F5CC3581F09B","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":"Q1945919$236FAD2E-1DA2-4AAA-9B97-084206632FCD","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":"Q1945919$61D626D6-BA0F-4A05-AE05-818184C822BA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4bad757aec17a8570e2102d57df4c93baefd6019","datavalue":{"value":{"time":"+2013-04-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1945919$66E413EC-07EB-43F2-80DA-865E5C9D8CC7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945919$4701AF45-B522-413B-B3A0-5D7B5357A4C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945919$ACEBC3B8-9151-4316-8DC0-9FCF00C08FAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945919$8D037F8C-75F1-4F1E-AF27-86F21C16AC52","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6d606ce38d15d835062997c6bd44eaf24b515501","datavalue":{"value":"6154940","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945919$070B1A81-A033-4014-87C8-1511169A41B8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b754569439d4565c57a4f9b6e4332c4f725dd3a3","datavalue":{"value":"\\texttt{Matita}","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945919$068F7AD0-95BA-4236-A4AC-8E58D0025F86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06abd77704a2a4cf160ef6bdfe9e8ffa3c8afd20","datavalue":{"value":"inversion principles","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945919$21DE414A-5D8F-407A-9EEE-8E1B22B3821C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50e42a98d1e220143db7aa919f32e078106ab7af","datavalue":{"value":"encoding of variable bindings","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945919$5756FC77-E7D4-4C93-8D74-ED7ED956F507","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945919$AB8831D5-4AA4-436D-8B7B-8805FA547EA3","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":"Q1945919$445F7333-B1FF-48D3-808E-7ABB9B5A821A","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":"Q1945919$EFB6C4FA-A74A-4C24-8B21-663F6D92BF92","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":"Q1945919$43D0F59E-33E2-4424-A686-7BEA4AA01B6C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8b85f856e323a188b6d6dacb380f12b7587c00e0","datavalue":{"value":"https://doi.org/10.1007/s10817-011-9228-z","type":"string"},"datatype":"url"},"type":"statement","id":"Q1945919$0AAAA12C-E054-409D-8F75-BA949D1EBEAB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aed0c84ffb280bf3c76cdc08948f7d34992e8fd3","datavalue":{"value":"W1982618236","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945919$38378438-63FA-4DD7-9D9C-08019A32AF59","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e9fd3039fb8a7242a39dbdcffc19371076ff91f8","datavalue":{"value":"Q126277594","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945919$55CB46B5-974A-4D8C-A406-A7478D18F223","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a1ae7aebac7ea3716330aa8760535123903599e","datavalue":{"value":{"entity-type":"item","numeric-id":1040007,"id":"Q1040007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945919$B4EC538A-824F-431F-A679-7C1097083CC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab98c2b4417373f1669b95e2ac3656950d8078a8","datavalue":{"value":{"entity-type":"item","numeric-id":3612433,"id":"Q3612433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945919$850CBB4B-FEE1-4757-BBAB-743FCA2B2260","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":"Q1945919$EC1D3263-15A3-4B95-B9D9-D8665E6A8B75","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":"Q1945919$13030F7A-AEB0-4544-B859-A478E4AD93E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c50237c8bde09d6668086722c62e1080ba158cf","datavalue":{"value":{"entity-type":"item","numeric-id":3189820,"id":"Q3189820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945919$FB5DFB59-5636-468F-BFE6-2291D3C26D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8be63c5f271ce7f1f200c26e0ab76283f6d86ebd","datavalue":{"value":{"entity-type":"item","numeric-id":1322473,"id":"Q1322473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945919$A2B9DE20-55AC-4A06-A2BF-060114D192AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5029f3bd44027d166b83affc49717f11751e7c08","datavalue":{"value":{"entity-type":"item","numeric-id":4736399,"id":"Q4736399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945919$2F18CDF9-1913-4784-994A-56BA4170CCC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b8c3a63f5113f0209622b58f18640a08a06fa7","datavalue":{"value":{"entity-type":"item","numeric-id":1887151,"id":"Q1887151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945919$AC5EB64C-22EC-4415-A1B9-7701A0ED73A5","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":"Q1945919$06E4D062-8D86-4210-8932-E951361EC46E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"25408402c90b88ebe7b3ea7c288dd36fab5576b5","datavalue":{"value":"10.1007/S10817-011-9228-Z","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945919$EF446FEB-0942-4767-8C68-194964460037","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"319f0e45bfa506ba9fbe0adbda954a115f9a8a53","datavalue":{"value":{"entity-type":"item","numeric-id":3189820,"id":"Q3189820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88e5f6753c7d02301cac62eb39ba19c45588318e","datavalue":{"value":{"amount":"+0.7958870530128479","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":"Q1945919$6B3ACA53-013E-4783-BACC-00BAF79CDD0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6a73d709232c759ceb44a34d554217041ef9d76","datavalue":{"value":{"entity-type":"item","numeric-id":1945915,"id":"Q1945915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0c504094e380c390729e88a689685b1a93e7993","datavalue":{"value":{"amount":"+0.7848074436187744","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":"Q1945919$7008A147-6CDD-4E24-B57B-06D98729A8B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51b15cbe5ea309bdc48ff40b9c5acde598f0666f","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"223304640e6575676a347d983bf36612f0ef62a4","datavalue":{"value":{"amount":"+0.7693042755126953","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":"Q1945919$609F85AC-3580-4B1B-84D2-5BC3A54EDDA5","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":"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":"Q1945919$205BB44A-7629-435C-9033-3D7E4B0ACA79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c485adaf5c9d59dfd696e67e8bfc3675d896cd0a","datavalue":{"value":{"entity-type":"item","numeric-id":4992397,"id":"Q4992397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90cc3ea8a2a5025aab2ad838719daadc84787c7b","datavalue":{"value":{"amount":"+0.7631136775016785","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":"Q1945919$6B4F5BEC-CD1E-4716-A231-6ABE93C78A3C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal metatheory of programming languages in the Matita interactive theorem prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_metatheory_of_programming_languages_in_the_Matita_interactive_theorem_prover"}}}}}