{"entities":{"Q5477643":{"pageid":7507202,"ns":120,"title":"Item:Q5477643","lastrevid":49872844,"modified":"2026-01-11T12:08:01Z","type":"item","id":"Q5477643","labels":{"en":{"language":"en","value":"Theorem Proving in Higher Order Logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5038920"}},"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":"Q5477643$6FE0689A-B249-44C9-B330-0486A954F682","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":"Q5477643$A376E14B-0D62-4DCE-841E-0D42B76BBCCD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5d9f532baf37dc64a641e5d6a1ef69163c1ad363","datavalue":{"value":"1152.68423","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477643$0399CC4F-6A40-43B2-AA2A-F4D2AAEDDDEE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"60e14ebe752857c79be86072108a2eaa35956999","datavalue":{"value":"10.1007/11541868","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477643$9F7F73A5-AE6B-491D-8B3A-AD4B0DDB6BF1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"de3fdac4ff0a76949283af3c275655aab2ae7465","datavalue":{"value":{"entity-type":"item","numeric-id":5477642,"id":"Q5477642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5477643$54FFCBB5-7138-427C-9116-46FDB2EFA9C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"af1ec9ad403b954308665ffc1e10cb99cc2fa4ad","datavalue":{"value":{"entity-type":"item","numeric-id":835775,"id":"Q835775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5477643$4BDE6D4B-4C8F-4C84-9BE1-BE4F9FC4FC8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"be1b81dbad9f9e73d0d9651b2f4eece3fcb4a994","datavalue":{"value":{"entity-type":"item","numeric-id":835776,"id":"Q835776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5477643$73EA6E61-8937-4516-86C6-1B5CAEC5E0A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce524b0c7940e9706063c12430e952a441c4e370","datavalue":{"value":{"entity-type":"item","numeric-id":290241,"id":"Q290241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5477643$01B7D320-4996-421D-8727-5C8D70F84D5A","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":"Q5477643$F110BFD3-94FF-40D5-AF86-1BCC9745D7F7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ab62ed9fc36983cf74c659518bd05672420ba04","datavalue":{"value":{"time":"+2006-07-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5477643$9E1B1984-11DA-4CA5-B892-2D6D15B3BE99","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477643$CE882DD8-ED48-4FF6-A399-C7F94EFE5034","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477643$687AADE0-24A9-4106-9111-46A14B8956E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477643$4AD6EC68-F965-4C57-8225-324B6CD024C7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"00e63c9237f02bd7bae7cd9ee59cae6dadf823d9","datavalue":{"value":"5038920","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477643$33772113-56BC-42C9-9004-9202375C32FB","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":"Q5477643$8E12B0A9-7F1E-4BD9-9005-0439F9862864","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c2fb76490c6ff834c9a8591f6e115d1ade34f149","datavalue":{"value":"https://doi.org/10.1007/11541868","type":"string"},"datatype":"url"},"type":"statement","id":"Q5477643$D703F8A7-8C2B-4DE7-8692-9BA15F836E8E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0c022af1b7546a705f000f89e81f31efc83cfd68","datavalue":{"value":"W2484880499","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477643$A6492D10-94DB-4847-8157-44493D9BF5EF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f296c0bc1ebf3b29250b6090d843bfb0b975f6cc","datavalue":{"value":{"entity-type":"item","numeric-id":3323253,"id":"Q3323253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b890c0e4dbc29197d1aaf3a23d3ccbe58e155323","datavalue":{"value":{"amount":"+0.7923067808151245","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":"Q5477643$37ADDD5F-501A-43CA-9E77-3D111E1D3141","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"983366cc153cae27be16c2535db5be25ad3578a6","datavalue":{"value":{"entity-type":"item","numeric-id":1040002,"id":"Q1040002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8e80e503b4723781ab63afe021cd11a0c658cf2","datavalue":{"value":{"amount":"+0.7864956259727478","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":"Q5477643$46188CFA-CEED-4D15-BF17-1454A9E1C13E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dab5f0dac86adcd3433b1b569367c23d0dfdd4b9","datavalue":{"value":{"entity-type":"item","numeric-id":4533015,"id":"Q4533015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"530e7f841f543626191cd97fe41aa66c3936e4d5","datavalue":{"value":{"amount":"+0.7766481041908264","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":"Q5477643$B4CF8647-B2FF-47D3-96A6-CABF4FD40937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36ed055ec8f5656036578820cd66c4de107a3a8d","datavalue":{"value":{"entity-type":"item","numeric-id":3067529,"id":"Q3067529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9af4444324a1a805ff53f1b4d060477730528d5","datavalue":{"value":{"amount":"+0.7653446793556213","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":"Q5477643$FFE57415-5883-4702-86EB-A578860B3C57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ed5d758f9568df2fc2c63e8fa6d923b7c7a8012","datavalue":{"value":{"entity-type":"item","numeric-id":1663225,"id":"Q1663225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a8072d275db3486101edf025fc83c1bc013097ef","datavalue":{"value":{"amount":"+0.7535858154296875","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":"Q5477643$6BE041AC-CB6C-4C2C-86F3-9DAAD80E6771","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5477643","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5477643"}}}}}