{"entities":{"Q5477644":{"pageid":7507203,"ns":120,"title":"Item:Q5477644","lastrevid":41200220,"modified":"2025-04-19T00:21:12Z","type":"item","id":"Q5477644","labels":{"en":{"language":"en","value":"Theorem Proving in Higher Order Logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5038921"}},"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":"Q5477644$222E359A-4FB2-4C97-B845-9FCFF882CE41","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0717c3cca11c13e40c60badbb849b8c4c08b303f","datavalue":{"value":"1152.68464","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477644$0108013E-1547-4125-912E-72F7CB6DA1C3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"60e14ebe752857c79be86072108a2eaa35956999","datavalue":{"value":"10.1007/11541868","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477644$1B682C8E-0A1E-4674-B8D5-C02A3448C70E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fde72a2d81cbfd58c1a2329aed776df473214803","datavalue":{"value":{"entity-type":"item","numeric-id":530842,"id":"Q530842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5477644$CE3041CD-F40A-4724-AA88-EFC0C84DF67C","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":"Q5477644$6947CA5E-11D3-4847-BB56-767A8A403965","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477644$7E137276-697D-4894-B328-F20E68770A78","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"73ec18ebf5652e8aaf4aff163e78a3dc5c13b246","datavalue":{"value":"5038921","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477644$125B6946-D628-4574-A1A3-A158503B6F75","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":"Q5477644$A6368E79-EC99-4445-81F3-09DAA679AB56","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":"Q5477644$FD31C964-5D3C-44FF-8D49-24DD6C3E6FED","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0c022af1b7546a705f000f89e81f31efc83cfd68","datavalue":{"value":"W2484880499","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5477644$69A08711-3E67-4CE3-B7C4-4B84D4DFBFC4","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":"Q5477644$7CD3BD0F-F2B1-48C5-8B8B-EAAE69D9AC65","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"936e77ea02442278ec9caaff7da6283b031f7089","datavalue":{"value":{"entity-type":"item","numeric-id":3546313,"id":"Q3546313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1b0f5131f6edf38fbc720148e9ca9874075db37","datavalue":{"value":{"amount":"+0.99999994","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":"Q5477644$50F79DAC-65FD-41A7-8F81-8BDBBEF3F089","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4abf5ace6955f8d6b99a9767bbc92970fa25cfda","datavalue":{"value":{"entity-type":"item","numeric-id":1744410,"id":"Q1744410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d716e356679ed2742688a8341489b89b2083ead4","datavalue":{"value":{"amount":"+0.8974086","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":"Q5477644$828BFF78-8A9D-4C26-9DEF-3CCD83E1A59B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2f3a66355419372373e528730b4767cb35f230ea","datavalue":{"value":{"entity-type":"item","numeric-id":4942633,"id":"Q4942633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae118efd4d219e5e3fa58ba4b41f4d0b74cdcebf","datavalue":{"value":{"amount":"+0.8756819","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":"Q5477644$7CF63E2A-6669-43C4-98CA-17010D248E86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7281a0001283fdab7726ccf6d153f33d8d948966","datavalue":{"value":{"entity-type":"item","numeric-id":4218093,"id":"Q4218093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cdcb9ef400831bfd95b5c1cbe702a8422cd51019","datavalue":{"value":{"amount":"+0.8756817","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":"Q5477644$9C7CA169-743D-4D65-85AD-7EFACC64FED5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b06f89c41d640daf3bd74f8f8e1b37397c2e2ac","datavalue":{"value":{"entity-type":"item","numeric-id":1412830,"id":"Q1412830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"508a5280e088e879422c964cb3d3f96ec8f60ab6","datavalue":{"value":{"amount":"+0.8732072","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":"Q5477644$4576CD2E-C282-45A9-BDB0-A03E50A00A49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46c5c7cc65fa7605d234cc789f21aa130bbc4dc1","datavalue":{"value":{"entity-type":"item","numeric-id":4474856,"id":"Q4474856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"549f6bb99f0be265ada8bbb6eb9e68fc529254fd","datavalue":{"value":{"amount":"+0.87110746","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":"Q5477644$EB2C52CD-6852-4432-864A-0EF9555D2D6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a9cb1b719bdefedb6d2fd80a527ce4ff1182d96","datavalue":{"value":{"entity-type":"item","numeric-id":3325711,"id":"Q3325711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c76f4b197ff28141fdb0519d74d3b5507196cb0","datavalue":{"value":{"amount":"+0.8694676","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":"Q5477644$A066EAE4-4375-4836-9257-EAC5EF3E2560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec1f642314305fda430872fabf19b330c6630590","datavalue":{"value":{"entity-type":"item","numeric-id":4302839,"id":"Q4302839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76ed42a09c1ce6e6cf275bafe8c5e7acd484d75b","datavalue":{"value":{"amount":"+0.8684878","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":"Q5477644$0BC0304C-2F0A-4B1B-9EBB-17C4E6B776DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"019f99791d45383943057206d50336b34a1727ce","datavalue":{"value":{"entity-type":"item","numeric-id":2981950,"id":"Q2981950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64e4afd7d5c3504af4ab6353212cbd50f96cd2cc","datavalue":{"value":{"amount":"+0.86511445","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":"Q5477644$4993F62A-1E36-4037-9B90-CBF49BFB1233","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14293c7b748a769cc6d7418d6a62065437805595","datavalue":{"value":{"entity-type":"item","numeric-id":5273440,"id":"Q5273440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25690e7d4ae80d5d499fefbe23f0b95140e6f36c","datavalue":{"value":{"amount":"+0.86432767","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":"Q5477644$B6CF6988-FD9D-4A09-AD75-700437DAE58E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5477644","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5477644"}}}}}