{"entities":{"Q2946633":{"pageid":2957353,"ns":120,"title":"Item:Q2946633","lastrevid":58062765,"modified":"2026-04-03T16:02:43Z","type":"item","id":"Q2946633","labels":{"en":{"language":"en","value":"Mechanizing the metatheory of LF"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6483140"}},"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":"Q2946633$0188AE7E-D5FB-4F35-A687-5AC9AA6429A8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a296ce2213cc8294df8f27d651b734d536ebb4ce","datavalue":{"value":{"text":"Mechanizing the metatheory of LF","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2946633$0D1C58C0-8726-4128-AAF3-2A3E559D5FDD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"53ef90da6629828ef2340fda6331ed04f8fff2b3","datavalue":{"value":"1351.68250","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946633$63C47A75-99CE-42D6-94C4-E72BBE79E85D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"946b7b8b2e0e573ffd0bed265d687cbc8d61be58","datavalue":{"value":"10.1145/1877714.1877721","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946633$DF84839F-C865-4583-833F-65C61BF452E3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8be13823e57b532010d417bfefa3b5133f759f9a","datavalue":{"value":{"entity-type":"item","numeric-id":860832,"id":"Q860832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946633$C1168993-66A1-4DDF-A262-9205536ED05D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5395fd6215daedab9dca2942f104c17e46b5bcc7","datavalue":{"value":{"entity-type":"item","numeric-id":616848,"id":"Q616848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946633$A2CDF931-9C43-4D0A-BAD3-0F3185BCD230","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"886664d698445e1702c39c62a8e99a722a88bdd6","datavalue":{"value":{"entity-type":"item","numeric-id":817699,"id":"Q817699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946633$A9706F5C-612D-46FD-B864-92E52D266105","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ae5381e7211b64f5f54296c18dfaf60be613ba86","datavalue":{"value":{"entity-type":"item","numeric-id":2946565,"id":"Q2946565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946633$219CB92B-5FA2-48DD-915F-E2A57D719C78","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ce093f9954be490f07dc8f1174896bb5ed4d11b0","datavalue":{"value":{"time":"+2015-09-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":"Q2946633$8964CA7E-3B57-4EC7-9432-EC509D6A3FD8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"46a1975c54033ed2be2bda038f6d4eaf07dd2b32","datavalue":{"value":"https://arxiv.org/abs/0804.1667","type":"string"},"datatype":"url"},"type":"statement","id":"Q2946633$A444ED03-C86E-4A7D-8142-BD458AE52970","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946633$7373DA46-3538-4C69-9E94-D21659CB647A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946633$F945F8C5-1359-4278-AC2A-038D89598E61","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"319c1db85de9e3eddf62f9d00712480013b9a052","datavalue":{"value":"6483140","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946633$13CCC076-7E99-417C-986B-85F9A57E1AB6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66040eec798fa7d182443c16b59531175d83cf5e","datavalue":{"value":"logical frameworks","type":"string"},"datatype":"string"},"type":"statement","id":"Q2946633$E1AB2455-9ABD-4183-BC65-0307FB751A91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"adecc22a9431064afad3f30ff1f0511d45170a4c","datavalue":{"value":"Nominal Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q2946633$627E5C60-9505-462C-97AA-5C7D3B1DA501","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b36661f0a3390102be2be05796702400601b738","datavalue":{"value":"theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q2946633$D12DAB5D-E513-42AE-B741-3C760E971098","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":"Q2946633$5FAE0059-9B1F-4C9F-ABE6-3DFF2BDCCD56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946633$6A8D30E3-1080-4060-8276-57FAF9BD23E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d40b61763c81cd80c5c82e03c39b2fdb5cbb80a2","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946633$EB998311-B91D-4C05-B216-D7F0465A53F4","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":"Q2946633$B42067BF-8F4F-4AE9-BA02-1F95DFD1AB9D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ed5eabfd2553900c33448f70cb18faabbc42f60e","datavalue":{"value":"W2077128347","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946633$7B749044-F2AF-4C4E-B8DF-6E9DCF27C65A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4a5467214381d9eb97275e6ca78397919ead761","datavalue":{"value":{"entity-type":"item","numeric-id":5308093,"id":"Q5308093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"204471d84165c32ee6ad7e41e1107beac2a871b5","datavalue":{"value":{"amount":"+0.91675484","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$2890AC63-9FE2-4E0B-8250-50851161E036","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd7140a2ae246559fc814817943371da5d5e1056","datavalue":{"value":{"entity-type":"item","numeric-id":2323447,"id":"Q2323447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e46813516668781cb1c52fc9b036f350db553357","datavalue":{"value":{"amount":"+0.89770776","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$518C6471-9B4D-4868-B9B8-4CF462B30F15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3246e880570cc8d3b53f9dbc1a60dacb4bd34c3a","datavalue":{"value":{"entity-type":"item","numeric-id":2844807,"id":"Q2844807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e849c298c41e34cdfe99a5029ab42b41f6a269c","datavalue":{"value":{"amount":"+0.8857582","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$312CEE43-4AD6-4C56-AA2D-4E22F5D666B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3653fa7595156c9eb48a6d6cfbdf97df9729312d","datavalue":{"value":{"entity-type":"item","numeric-id":2849493,"id":"Q2849493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"55474842f901a7304229aaa65a486192f698c8d6","datavalue":{"value":{"amount":"+0.8826583","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$4D5709C3-E66F-407B-AD74-79D40EF3BC7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14369c1b2b26c1a5adfc89152eb76e189196af45","datavalue":{"value":{"entity-type":"item","numeric-id":3189797,"id":"Q3189797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb4d6f8fbb54f64cc317a1492f4f4e4bc82f0e9e","datavalue":{"value":{"amount":"+0.8811478","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$61835ECF-31E5-4383-9BDE-C0F53F40DA45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3ef072fb71a8f1cd37ad6a71751c23ae314c430","datavalue":{"value":{"entity-type":"item","numeric-id":4249901,"id":"Q4249901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42aa5fb57456dd07e83efd30005b92326af87621","datavalue":{"value":{"amount":"+0.8717379","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$F021BE10-2CA1-4F65-96F3-AF3EFA963DCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f32f7afc6645b673602a57956dc8615f52a3e28","datavalue":{"value":{"entity-type":"item","numeric-id":2352491,"id":"Q2352491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3871253c6a30d1b1e9a13081b575684fa3bfe0a3","datavalue":{"value":{"amount":"+0.8691718","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$799FE107-3D40-414C-879D-57E1FF7602EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16db67012b2077f5bad56f6e6e6bfa4f8ae41098","datavalue":{"value":{"entity-type":"item","numeric-id":2676562,"id":"Q2676562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae368685d8f5b71c6c861f3f67f5b5aa7e5ac883","datavalue":{"value":{"amount":"+0.86427873","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$73C57683-8F88-43AB-B154-A3EBA2075542","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"379e0292ca3acb9bd4c247f3239b0373dd09f4da","datavalue":{"value":{"entity-type":"item","numeric-id":1945921,"id":"Q1945921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2f687f7f518afa57d630b17cf4c3dffee1dcc22","datavalue":{"value":{"amount":"+0.8613683","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2946633$B89E11DC-A9EE-4A38-BDFC-64622607A64F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2946633","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2946633"}}}}}