{"entities":{"Q5438966":{"pageid":7468530,"ns":120,"title":"Item:Q5438966","lastrevid":50269736,"modified":"2026-01-13T17:11:49Z","type":"item","id":"Q5438966","labels":{"en":{"language":"en","value":"Type theory and proof processing systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5233465"}},"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":"Q5438966$4BC16F75-ED3C-4DD2-A6CA-83692CDD0F44","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dc96ad6f1baa852881bf4335fe20c782715adc2b","datavalue":{"value":"1127.03319","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5438966$DCA39285-2A78-4A74-9276-96A3DD0815C2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f681530f1e601559ae451198ac16d4e80569d32e","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5438966$9A27E47B-14D7-4B64-A78D-2441072298AB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"67e2a9a878a2213f3076b62fafd86632f88b9875","datavalue":{"value":{"time":"+2008-02-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5438966$79E82953-0F0C-4FFE-A4FB-09B0BD7EDAA2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5438966$E3419EE5-C667-4278-99E9-74E27EF7453B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5438966$DAEA6ABD-BF81-42EC-B3C1-69EE99A5D8E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5438966$694406BD-6481-4FA6-9F1E-9A87FD25F31E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9eef0a3c832d9c05fc919dd941df7776595a5570","datavalue":{"value":"5233465","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5438966$DB43E494-58E8-4350-BE03-47E6CD58E0ED","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c207a2596caed3e2cac45685d28c7c6980375ae2","datavalue":{"value":"proof processing system","type":"string"},"datatype":"string"},"type":"statement","id":"Q5438966$8F44CA81-DEF8-4C4C-93F3-731F256F1B64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5438966$0DF1658F-7892-479A-95DE-782856556CE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b36a4092864d39bf9c99c5936b3d1261e44b9950","datavalue":{"value":"set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5438966$C608CF4B-BCDB-4E74-9E49-1FA89EEAD307","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0c1f8ecbef520debe4ed65c00c0dc97890c1127","datavalue":{"value":"proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q5438966$BF2BF40A-9765-4382-B783-8AB2928F34A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b399e80d32f01f0e5ecb7d27abf0eef31abf6cda","datavalue":{"value":"deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5438966$62CCADD8-F49E-4C9C-9223-85EE67F94CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"90b2ed3c130c30bac7174fa9b54a06645cc1227f","datavalue":{"value":"computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5438966$4A7D137F-909E-4F48-B8D0-2B026C338BB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d65cdbc3eb134bc5f78d89f3fc9f703a3e4c38e1","datavalue":{"value":"mathematical language","type":"string"},"datatype":"string"},"type":"statement","id":"Q5438966$C074DA53-CE53-404D-9A9D-D26034ACA5EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9c0b9f590f9c7db6794b6e6756c05cf4e7719a63","datavalue":{"value":"function","type":"string"},"datatype":"string"},"type":"statement","id":"Q5438966$2F6F77EE-AC98-4122-B6BE-DF6970C624F5","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":"Q5438966$1CC8E845-AFD0-40E3-87C0-D252EAFC9D03","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5ee6f886ef0705827062d0a4c87d655476ba33e","datavalue":{"value":{"entity-type":"item","numeric-id":4204148,"id":"Q4204148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a41c77e24723898726cb52d39c02517a8703f3a","datavalue":{"value":{"amount":"+0.7762382626533508","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":"Q5438966$F32B4219-1EF4-4F93-A449-349DB77AFEF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"776a7f81bcf627160ac001fd4998e9de8ac0400e","datavalue":{"value":{"entity-type":"item","numeric-id":4215639,"id":"Q4215639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"781095ee8d04d250d86d8ce93fcb744e47679e55","datavalue":{"value":{"amount":"+0.7648602724075317","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":"Q5438966$FC25ACCA-78E3-4994-8C95-7117B6F2094E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b215bf34512acd6bcf522fcb8600bc4a72a5aa95","datavalue":{"value":{"entity-type":"item","numeric-id":4289277,"id":"Q4289277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f76e16950d9c6e919d6e52108044eb22dd8fc79","datavalue":{"value":{"amount":"+0.7629219889640808","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":"Q5438966$EF1E0538-9508-4E28-BCF9-33027B9D2024","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"787bce44c26bfa68c4bdd6a337d32f1925d9a163","datavalue":{"value":{"entity-type":"item","numeric-id":3757915,"id":"Q3757915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b5d4547ae35a5bca1f5b7191f4cd15739370bd47","datavalue":{"value":{"amount":"+0.7486448287963867","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":"Q5438966$E97CD411-0D33-471C-88E1-46AE15F063FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab32e2ed94b731d98c2de454df33bbc9733c6c09","datavalue":{"value":{"entity-type":"item","numeric-id":4246941,"id":"Q4246941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54e5c7b1320ebec1a0a3977b92669aebc7254fd1","datavalue":{"value":{"amount":"+0.746567964553833","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":"Q5438966$6487D4F8-71D2-4FC1-BA19-095C3550CF24","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5438966","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5438966"}}}}}