{"entities":{"Q3608422":{"pageid":5638328,"ns":120,"title":"Item:Q3608422","lastrevid":58214112,"modified":"2026-04-04T06:31:25Z","type":"item","id":"Q3608422","labels":{"en":{"language":"en","value":"Building Decision Procedures in the Calculus of Inductive Constructions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5523403"}},"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":"Q3608422$1DD96D1D-9D56-423E-813B-45BD1A6C78A6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8727dc5fe82de3d7ac29b1f83fe91ed190a52ff0","datavalue":{"value":{"text":"Building Decision Procedures in the Calculus of Inductive Constructions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3608422$A8FFFED3-386B-4825-8536-DC8F9BE813D7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ccfbefcc4ee37b173653af4e3c79acb905a8c1af","datavalue":{"value":"1179.68135","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608422$45F4050C-AF12-4C1B-8B2C-D85669E30BBD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3f6bf37caa6990cbd2e358a99230192bef7677c8","datavalue":{"value":"10.1007/978-3-540-74915-8_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608422$84BB68B7-ABEA-4F9B-9E1B-3C65D4CCC9D0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8807e9b5ca6f3e9539fb2629b3f3fe474d0fb0ea","datavalue":{"value":{"entity-type":"item","numeric-id":235598,"id":"Q235598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608422$8A4711B9-FE0F-4090-83DD-9BC2772CA5B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1b1bfbcb4e8f5871a00d29a6022e3016b3479851","datavalue":{"value":{"entity-type":"item","numeric-id":235599,"id":"Q235599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608422$372DCEE0-E23F-44A2-B9A4-05EFE29263E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1745bdeb092262739da6d0fd18a64d1c3c06446d","datavalue":{"value":{"entity-type":"item","numeric-id":2323969,"id":"Q2323969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608422$A9239213-000A-47CD-98CE-CE2D410E1E8F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6ce06ac78cec2c642b9fbad4cd2a2e4121754d54","datavalue":{"value":{"entity-type":"item","numeric-id":3540165,"id":"Q3540165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608422$1B9FE31F-17AF-43CA-A7B6-CBFC7E9E837B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e03d4b2ec538fbc0e4998d600e67e2b2cfa008b2","datavalue":{"value":{"time":"+2009-03-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3608422$ED38FEAB-EBED-49C3-8C11-18A9D8094E5D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"194b7983997d3d74a6d349f2175110bccc711e47","datavalue":{"value":"https://arxiv.org/abs/0707.1266","type":"string"},"datatype":"url"},"type":"statement","id":"Q3608422$94556970-01EF-4FD4-A669-0BC81CAC9F0B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608422$A3AA9BC9-9415-46FF-84FC-9D663B318081","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608422$392735D3-D2F3-4D43-8FAA-FBE557968362","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608422$7D4E5D58-B815-478E-B1A5-35F6B5570C22","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b43af9c461aa09f37e2f691b5c925383406f3e17","datavalue":{"value":"5523403","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608422$2D13CA4B-106D-497B-9DC3-441D0EBF95DF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ee22a16b68ff7690ced49d39b0f7a8a6db96b60","datavalue":{"value":"calculus of inductive constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608422$869C9671-54AF-46BD-834E-7F7641D6A288","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608422$10C86CE5-1F81-4CE9-9568-4697E54F40CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b36661f0a3390102be2be05796702400601b738","datavalue":{"value":"theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608422$700D18C5-2BE4-41E9-8096-896054250885","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608422$E6EE6EA5-C287-499E-8DDE-A6DD2B872C25","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":"Q3608422$E1589C43-1A9C-4981-A7F8-C65EAC80935A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7553c06c96f99bd67fba18a4416e6b0bf95a7ace","datavalue":{"value":"W1628824908","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608422$33ED77D4-98B1-4F64-B520-DFD98FBCBC2B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7e4e5f69ac10da5dfbf809d1b24702f6902e7150","datavalue":{"value":{"entity-type":"item","numeric-id":5747669,"id":"Q5747669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3675ef88ed3e146adb1ff9026cd4f33de635db98","datavalue":{"value":{"amount":"+0.9217164","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":"Q3608422$A3A1B135-5B38-4F99-8FA4-954D19DFF01E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a299ada1677cb50f9badc2dfb747cce9998463ae","datavalue":{"value":{"entity-type":"item","numeric-id":3026376,"id":"Q3026376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c8b172849974ef7c42a7528aa366fc308b1d98b","datavalue":{"value":{"amount":"+0.91581917","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":"Q3608422$8DF17C9D-DD15-401A-9A18-AC9A26CA0FE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a60c342ca70b6a001e5ab65f9968fc1d0ec10393","datavalue":{"value":{"entity-type":"item","numeric-id":3805882,"id":"Q3805882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c8b172849974ef7c42a7528aa366fc308b1d98b","datavalue":{"value":{"amount":"+0.91581917","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":"Q3608422$ECE6AA52-4E1E-4095-A1E6-3155D3E8A447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca926648b6e53da805b017264eca5f653bace98d","datavalue":{"value":{"entity-type":"item","numeric-id":5712303,"id":"Q5712303"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f9d6af7e38105932bb870776dfbb275696cd3b1","datavalue":{"value":{"amount":"+0.89993346","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":"Q3608422$BC65E343-0F7F-492A-AA2F-70AB8D2BFB67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd6c4658e500acac07a786b65bb37fefea5676ae","datavalue":{"value":{"entity-type":"item","numeric-id":5881199,"id":"Q5881199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92ee11387d394afd929f681875eac1e408f806a5","datavalue":{"value":{"amount":"+0.87662333","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":"Q3608422$B05D16B6-3457-4F1A-A111-144578C6D5EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04d3059def3a1d11991a42b48d069012b0de3f3f","datavalue":{"value":{"entity-type":"item","numeric-id":3638245,"id":"Q3638245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f0053d7efbf86f5941251f0d49bd5548f43d1af","datavalue":{"value":{"amount":"+0.8762036","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":"Q3608422$1679F9BD-8639-4D42-A116-AB6743910D81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e0b4f8dc50ecd9e12007dc74c0a573be2d9ec78","datavalue":{"value":{"entity-type":"item","numeric-id":4430633,"id":"Q4430633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd5dae9bf28999c02208d52185986d382356eaab","datavalue":{"value":{"amount":"+0.8757961","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":"Q3608422$FE248B77-C0DA-4A0A-9821-1E6049946643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de1725feaf53bf8d1375b89f093885a013eaaf4f","datavalue":{"value":{"entity-type":"item","numeric-id":2844811,"id":"Q2844811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e605a87692b79151578a3a1555250f62e474b25b","datavalue":{"value":{"amount":"+0.8757293","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":"Q3608422$631DAD82-DD03-4779-8814-7FA0F0B6C1F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4acd3fa3f3bdc0687f761d59bb22ea5724db5aa","datavalue":{"value":{"entity-type":"item","numeric-id":5387883,"id":"Q5387883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0be476cef94a0a45a5d6bafc4680a26ba85ec277","datavalue":{"value":{"amount":"+0.8737867","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":"Q3608422$4B87754C-A6DE-432E-B70B-7104FD359E38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd6d437810c57cc5debbc20171e5f9d59bdb9772","datavalue":{"value":{"entity-type":"item","numeric-id":1040007,"id":"Q1040007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d7bb09174dea4b394c9d63253c5dc6976c13613","datavalue":{"value":{"amount":"+0.8720379","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":"Q3608422$28A3DCFC-6930-4115-AF00-242B61AF6C76","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3608422","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3608422"}}}}}