{"entities":{"Q5477661":{"pageid":7507220,"ns":120,"title":"Item:Q5477661","lastrevid":92395712,"modified":"2026-06-05T01:37:06Z","type":"item","id":"Q5477661","labels":{"en":{"language":"en","value":"Theorem Proving in Higher Order Logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5038936"}},"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":"Q5477661$5C26C5E0-F25B-4EDC-9972-FFC5BF308634","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":"Q5477661$9E7D1476-3E03-486F-8897-B9E8B2B513C0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"46f0fcf2ae3d1d86a11e416fc9330b231f7de87f","datavalue":{"value":"1152.68532","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477661$71A601FB-9914-465F-830B-0DCCEABE1C33","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"60e14ebe752857c79be86072108a2eaa35956999","datavalue":{"value":"10.1007/11541868","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477661$7B2B77E9-3305-487C-A511-FAFDB24B8D71","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad9237ea02bde72f8eb7465bdbc297d9942104e1","datavalue":{"value":{"entity-type":"item","numeric-id":5477660,"id":"Q5477660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5477661$3D904940-C000-4F1E-B6D4-F8326FFE2ED5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa9c0912ece4e82f4f9a482c387448e9bc57b15b","datavalue":{"value":{"entity-type":"item","numeric-id":835777,"id":"Q835777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5477661$C00B000F-A368-46EA-97DE-BA9BB2668C89","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":"Q5477661$B7BB6737-4F93-441E-9701-C71092D71465","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":"Q5477661$8A16528A-6E0B-4CED-972E-9B74F81AC848","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477661$36E6A3E9-A2C4-479F-A26F-96EC57DDF938","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7dde57cbaf704d564d8f981ca98d6340e3d4aaf","datavalue":{"value":"68Q05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477661$14043868-C1B4-4AD3-9DCB-86BAFB994DF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477661$F0E15620-22E5-4B06-9EBA-2CD03D756B3F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"52d901040fcf5c08840ead44cd2e18c7dfc9fb7f","datavalue":{"value":"5038936","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477661$E36B3DDA-0FF4-4DF6-87B6-F9629F5FBDAC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5477661$D606D319-0C1C-4A4A-B739-AF768425F5D6","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":"Q5477661$0DEA1C5D-176F-4F05-B7D8-08D75EE8BA12","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":"Q5477661$2322E853-56AB-489B-9308-5F4C666B7C3E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0c022af1b7546a705f000f89e81f31efc83cfd68","datavalue":{"value":"W2484880499","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477661$30E60788-66FD-4A0F-8474-8682F46AE98A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc708f7490838cd9f7ac31978684132580c81890","datavalue":{"value":{"entity-type":"item","numeric-id":2722044,"id":"Q2722044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e262a924133a6d0109e80e6249c0323922241a5c","datavalue":{"value":{"amount":"+0.81496483","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":"Q5477661$010A8758-8F0F-4BF5-A80C-CDF5A65CDA2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f08f45d9e7056e96ec5a16090d6f5caacc2182f2","datavalue":{"value":{"entity-type":"item","numeric-id":4736996,"id":"Q4736996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fd8eee82218774e220e0b6c84d98b13c1e70caf2","datavalue":{"value":{"amount":"+0.81362677","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":"Q5477661$6D477E1F-DA13-40EB-A868-37904E241363","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c08b12e2e57d200144a65bfc6cd29d62405e5254","datavalue":{"value":{"entity-type":"item","numeric-id":5492995,"id":"Q5492995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15fdbc34f4b5036394c1ad7044f7dd02bdd48843","datavalue":{"value":{"amount":"+0.811602","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":"Q5477661$0D43D5D9-8C83-4B42-AE3B-960112FACAB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77c789d9a6d2ec93ba00de3ca763678a1cf6dfee","datavalue":{"value":{"entity-type":"item","numeric-id":5899154,"id":"Q5899154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bace70d9360c223e263ce519a00afc9b391519d9","datavalue":{"value":{"amount":"+0.8082166","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":"Q5477661$D842CDCD-038D-480E-9A04-249558304AD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"373accb42c22b62b51bc441ddc14c88d9c0f7027","datavalue":{"value":{"entity-type":"item","numeric-id":3176366,"id":"Q3176366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1fc734826fba0719eb9039ffd928a4b3ec3b62c","datavalue":{"value":{"amount":"+0.8080598","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":"Q5477661$4BCA5767-7337-4AB2-9FA8-57B0E0BC06BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e61b7dad93d58c2ff581f55645a5dc1938938fa9","datavalue":{"value":{"entity-type":"item","numeric-id":3421467,"id":"Q3421467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d299ac7e10a20f7443896f604844743ead0995f","datavalue":{"value":{"amount":"+0.8062012","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":"Q5477661$3FA767B9-A701-49F4-983C-6E6960E842E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aadc653ea280c6112ef77db1a31a0f4403929e29","datavalue":{"value":{"entity-type":"item","numeric-id":5756614,"id":"Q5756614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cdd3d396f564fbe7c6008591b21f374957d87f2","datavalue":{"value":{"amount":"+0.8053601","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":"Q5477661$47A64D83-8707-4910-ABEE-51DB268E9E7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad1b4c8ca56d035652b395bc9f4cf5d301d7d108","datavalue":{"value":{"entity-type":"item","numeric-id":4411151,"id":"Q4411151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64c9c2bfa845b64dce715ab20974d74d201100c7","datavalue":{"value":{"amount":"+0.8030337","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":"Q5477661$10A84007-CCD4-4B18-9218-BA2F78BBD301","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71655a21c698dab22e4e8cf07f26f9de96228222","datavalue":{"value":{"entity-type":"item","numeric-id":3629888,"id":"Q3629888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"58c83997f7c95a228fb62cdb3d05af06c4712823","datavalue":{"value":{"amount":"+0.79971695","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":"Q5477661$1A4AAC04-4D22-4847-B231-BFF7921BB443","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa4b9d54b0da3c4115311f34cdbd4e695260e620","datavalue":{"value":{"entity-type":"item","numeric-id":4536108,"id":"Q4536108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ba213aea6970dec76da723639ce83ae0f46e357","datavalue":{"value":{"amount":"+0.79532665","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":"Q5477661$5D474BBD-1CD4-4367-8BE0-5AE90DFDE7C1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theorem Proving in Higher Order Logics (scientific article; zbMATH DE number 5038936)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theorem_Proving_in_Higher_Order_Logics_(scientific_article;_zbMATH_DE_number_5038936)"}}}}}