{"entities":{"Q4647555":{"pageid":6677136,"ns":120,"title":"Item:Q4647555","lastrevid":82241714,"modified":"2026-05-06T20:26:15Z","type":"item","id":"Q4647555","labels":{"en":{"language":"en","value":"Proof search with set variable instantiation in the calculus of constructions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001944"}},"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":"Q4647555$DF9E3D2C-057B-4A15-92F2-C92D83AAEC58","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d9038fe8932e6c955255fa7be6acb5fa95fe684e","datavalue":{"value":{"text":"Proof search with set variable instantiation in the Calculus of Constructions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647555$A9D3D60A-F6BF-40AA-ADA6-F6835E89923B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a02827f5ca631b1846414c3b86a2c4afb837f9cc","datavalue":{"value":"1412.68221","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647555$BE1EDB72-8B7A-46B9-A7ED-9D880AE36234","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4567c76c81b5cfbe60727be95ef9d6e5fa7c3a15","datavalue":{"value":"10.1007/3-540-61511-3_120","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647555$74336F52-49BA-4E3D-B017-EEB07714192C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$19598304-494D-400E-A936-C327B2A7A7D9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647555$BF3E3448-CA71-43DB-87E0-84D4C238B2F3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647555$3BB84346-6E56-4576-BB8B-BC1E55A4B1F6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5bf5038f7b9330596037ada0589324903977547c","datavalue":{"value":"7001944","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647555$BDD286AD-F230-4428-A7BF-2984574C70D3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c3098c31aaa054039cc5414efb85f4a6bce38102","datavalue":{"value":{"entity-type":"item","numeric-id":590551,"id":"Q590551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$96E8ADF9-8742-4CF2-838B-6FB8B266B5B0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$C312D8FA-B963-4390-B8AC-CAD414E97E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$A10DED66-905F-46CC-B878-A46967936C2A","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":"Q4647555$FB18E31A-0FD5-4099-9485-99BA39A72253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$988B4C93-0350-4C96-BA13-2976CB8505DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$05213EDB-AEED-46D2-B46F-A0080ED23074","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":"Q4647555$FC4F4361-D091-4371-93EF-167810F3A379","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fe4e1e0ddd93d659c5c85a1b944d313481ab60eb","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_120","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647555$DE2EC1EF-4B5B-4966-888B-F9E5CCE80D69","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"697a4315e395b2a21ade15b1b5f1d2eb503c7104","datavalue":{"value":"W1514169328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647555$BF5FDBFC-5A6F-4D0B-A1AD-4E9BFC4442DB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b3cd1e4c8a325fa7e9a7d1a0eb085324974feda","datavalue":{"value":{"entity-type":"item","numeric-id":1319387,"id":"Q1319387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$00368FAD-FA7B-4167-8FDD-D7F9545AB004","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$8A1C12E4-4D1E-423F-9D47-69D7C9FF3462","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$23F38A57-93D8-42FF-B022-2422E5F8A111","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ac899433a8e17454dc938a2d4fc8f05db348c5e","datavalue":{"value":{"entity-type":"item","numeric-id":4871733,"id":"Q4871733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$9C50A538-B921-4A08-B838-2AFA71BBEFC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"774c18fd2b844ce5d75610805893e277658a480f","datavalue":{"value":{"entity-type":"item","numeric-id":4276174,"id":"Q4276174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$9DE7F9B4-5197-42BE-8E88-385D416F2285","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$297C9E1A-E302-41F0-AB65-5C9D2BBAAC97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$F745FFBF-8ED8-4B3A-9F3C-0E00DA823A0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c9e886b9360a3e41cc1b6bf60219a57e89b7504","datavalue":{"value":{"entity-type":"item","numeric-id":4692468,"id":"Q4692468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$5965085F-CD54-44FA-8EB2-118995465389","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aebd32d099ee8c91552756addce4fb86715ed2d8","datavalue":{"value":{"entity-type":"item","numeric-id":2640596,"id":"Q2640596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$E3460787-7253-4C85-928E-8283A10496B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647555$3894455B-7DB8-4236-8F30-728D4AB60A76","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"099ae0f1e97a5570afaf6cbcd85e391e984ef7f7","datavalue":{"value":{"entity-type":"item","numeric-id":1575927,"id":"Q1575927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"972ef5181b49c72c73b2d6c6bb8f4a20f4b87d10","datavalue":{"value":{"amount":"+0.9534271359443665","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":"Q4647555$1D8D505E-62DC-425E-AFD1-69E2551C54C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"050391e3f27b8bfab5af09f69bc4e968903fe067","datavalue":{"value":{"entity-type":"item","numeric-id":4871733,"id":"Q4871733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db660277d82aff2175bea94f936a068a8d057a3b","datavalue":{"value":{"amount":"+0.7553357481956482","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":"Q4647555$9259B040-EA85-4A06-9603-310194A46B46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8293d39b4e139795d4cbfc0c1170fc2b9210bed3","datavalue":{"value":{"entity-type":"item","numeric-id":6488534,"id":"Q6488534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"104064095d4d72d525ea1c03801de109c77d402d","datavalue":{"value":{"amount":"+0.7400348782539368","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":"Q4647555$888EFEAC-2940-40B2-9237-139B4036170B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba5ddd592d5b38bbc2651085afdaabc9d3ec7901","datavalue":{"value":{"entity-type":"item","numeric-id":3586992,"id":"Q3586992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"871e7ff328fb0555f029752e305cff2a05909675","datavalue":{"value":{"amount":"+0.7284023761749268","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":"Q4647555$7BC969BB-CE54-46BA-AD32-55C741EE9AE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bee04c484d535e2047ff41467496515c615b4695","datavalue":{"value":{"entity-type":"item","numeric-id":4809075,"id":"Q4809075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7dbd6338296663234f560357221474be52b0a873","datavalue":{"value":{"amount":"+0.7254256010055542","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":"Q4647555$BD9B02D9-5271-4415-9AC0-692FE213E680","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof search with set variable instantiation in the calculus of constructions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_search_with_set_variable_instantiation_in_the_calculus_of_constructions"}}}}}