{"entities":{"Q5464653":{"pageid":7494212,"ns":120,"title":"Item:Q5464653","lastrevid":92567435,"modified":"2026-06-05T02:02:20Z","type":"item","id":"Q5464653","labels":{"en":{"language":"en","value":"Theorem Proving in Higher Order Logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2195667"}},"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":"Q5464653$59C705D4-25F2-4DD7-9BFE-BDA01A06B0C9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1dbf86f36180251007d930e80e9af96d205b11ea","datavalue":{"value":{"text":"Theorem Proving in Higher Order Logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5464653$B0CDCC72-4609-4FFD-9CE9-8E34C8A7CF1A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0a489ac6e0de76c027598558e9ccfa27cf6f1dd8","datavalue":{"value":"1099.68526","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5464653$F96816B5-84B1-4E9E-8DD0-09C5CD7FFE7C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"576402c0dea459a726c2e69c990ec7ad30beb5e0","datavalue":{"value":{"entity-type":"item","numeric-id":539419,"id":"Q539419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5464653$3CA4619D-6768-4572-8535-3BC23495A150","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d6ac8467bb8819c8ae7927627c8311222acd3f38","datavalue":{"value":{"entity-type":"item","numeric-id":5464651,"id":"Q5464651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5464653$25B9D516-9E91-4899-9224-49EC24A1EAB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8fa2d2ab03353064aadef64c52f4fc44d8aeecf","datavalue":{"value":{"entity-type":"item","numeric-id":5464652,"id":"Q5464652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5464653$E59E7B59-143F-41F9-AF20-0FC750AB49A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2daae3e1c4a91d851e44eeb961260350c6d531d3","datavalue":{"value":{"entity-type":"item","numeric-id":851145,"id":"Q851145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5464653$7F6E6CC2-6F95-4248-B8F1-850263BDABD2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5464653$A169FE89-B643-4B72-858A-6891318A09E5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ddb11065d0a8b2eb0c9ba922644fcd7df350e36a","datavalue":{"value":{"time":"+2005-08-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5464653$1952BF5B-73A4-4195-A825-4E839F69CF32","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ff42057022552eaa82447a5a1563ef3bf93acd","datavalue":{"value":"68M14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5464653$3F77D070-4718-494F-B6EA-450D4641B291","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8d8a22ace48964288ca1ed080fca5299ff532395","datavalue":{"value":"68M15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5464653$1CE9EC14-7B26-4EA6-B46E-268696683179","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5464653$692F7DF2-691D-4C7D-ABC5-54811E742DE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5464653$33691262-7B6F-4FE8-9F2B-152F14B083B0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"453b76cfcd2f0acb3d95360ba294456b563e7b36","datavalue":{"value":"2195667","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5464653$5F78FF99-1CB8-4E4D-8F44-0E9EAB6AF385","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5464653$1A7E738C-8BE3-42A8-BF10-3F06AACA875B","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":"Q5464653$B3E45E29-470E-42DD-9CA5-BFDF61BFE9F4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6d0827adfce9e95a41e9b241cb6e71fc5161e244","datavalue":{"value":"https://doi.org/10.1007/b100400","type":"string"},"datatype":"url"},"type":"statement","id":"Q5464653$384151F8-490D-4F2E-972B-467AC2D170F2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3e2331554d07e306ad1c5f27a2ceb70ff59729ae","datavalue":{"value":"W2798038182","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5464653$A80770F5-85E0-4A99-AF73-5645ED458D5B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c8f3c87052d3eba7f583a529fee7b521492998e1","datavalue":{"value":"10.1007/B100400","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5464653$EF7A2F0A-BDAC-426C-9DD0-5328E1924018","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b08bde013cf4a00f7bcdfc21c42c0c93358a1ae","datavalue":{"value":{"entity-type":"item","numeric-id":685095,"id":"Q685095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"465089f31ff43760e907caeaf565aa409b98bc2b","datavalue":{"value":{"amount":"+0.91827655","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5464653$5634C035-3262-4E55-BCAD-01D17FC895EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bfd3bbf30be09137a4af2ce28feff9e537b2f311","datavalue":{"value":{"entity-type":"item","numeric-id":5275399,"id":"Q5275399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a241941dbc59a7e0e7ded8ff3714f3e823ed89a","datavalue":{"value":{"amount":"+0.9173317","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5464653$5E8CFA16-6150-4968-8A1D-853CC4EE0B27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"facfb391b37b0c2d59677ab220d021147e52d1a8","datavalue":{"value":{"entity-type":"item","numeric-id":2011199,"id":"Q2011199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6783dd33cc1febcbbf4f779730d56b6bff8c460c","datavalue":{"value":{"amount":"+0.9148217","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5464653$B1341BCD-7B9E-4169-8206-38297E987F60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"058191dc2c9d3bf412333ced6fa3ff5c09a51638","datavalue":{"value":{"entity-type":"item","numeric-id":5458335,"id":"Q5458335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"05ee28e63aab39d2fbf572c262019ab3ed0d7b4e","datavalue":{"value":{"amount":"+0.91326964","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5464653$EB7C2D39-6506-451A-A856-8F3CBB4E9849","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"70105a902ce52300c8b5ffb4b3b3fb179f59bac4","datavalue":{"value":{"entity-type":"item","numeric-id":3043807,"id":"Q3043807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9ed6cc5ae1cca6964b4a4eb74fa44fc0db84fdd","datavalue":{"value":{"amount":"+0.9130739","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5464653$C4F01B1E-E456-4E26-8751-89C884DF8EB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd0dab15aebde0a981bf588cf769f7ffff92a844","datavalue":{"value":{"entity-type":"item","numeric-id":5137900,"id":"Q5137900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eea05055ef855fb9f45437bda2d3843d5dc14835","datavalue":{"value":{"amount":"+0.91219515","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5464653$94F1EA7A-E483-4E2C-9414-F3D988F22240","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"17a6af207576128f1cb824b42f378b5086130701","datavalue":{"value":{"entity-type":"item","numeric-id":5261538,"id":"Q5261538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c61f577cca0e9a45fedb5aeea8812b787aca4a8","datavalue":{"value":{"amount":"+0.9075755","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5464653$6723766B-E4A4-4542-81A9-044D78D4500E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theorem Proving in Higher Order Logics (scientific article; zbMATH DE number 2195667)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theorem_Proving_in_Higher_Order_Logics_(scientific_article;_zbMATH_DE_number_2195667)"}}}}}