{"entities":{"Q5234717":{"pageid":7264285,"ns":120,"title":"Item:Q5234717","lastrevid":94688753,"modified":"2026-06-05T07:28:47Z","type":"item","id":"Q5234717","labels":{"en":{"language":"en","value":"Hybrid interactive theorem proving using Nuprl and HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7111187"}},"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":"Q5234717$57BBA7DD-9547-4900-A431-89AF285D8561","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"eff07c25b5e79fede75247ebc5a0805279a5b561","datavalue":{"value":{"text":"Hybrid interactive theorem proving using nuprl and HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5234717$6AE652C2-1087-4C51-8584-067A9C27AA1E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1e3367cb87b0af149b27a6e1c0bec40a0ee992fa","datavalue":{"value":"1430.68403","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234717$3D795A12-978F-4AA8-8567-3DF8BBD8A948","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"514381a32df2c6931d1ea0fbcace286f4c18d278","datavalue":{"value":"10.1007/3-540-63104-6_34","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234717$7530FCF6-ACD5-4D11-87E3-FC4CC4C77E2A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3d3860a2f9767fdefbee4661adcdc84432183bcd","datavalue":{"value":{"entity-type":"item","numeric-id":5234680,"id":"Q5234680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$A4BA2F76-84E8-4FD9-B0D1-EBE163E695EC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"dea1ace5968cb70ccc50b025abd55a0016bafdf0","datavalue":{"value":{"time":"+2019-10-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5234717$E4C0C8DD-7374-4BA5-8F2E-CADED4A842CF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234717$04F30DEB-523D-4399-A148-E1B23C4FAB12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234717$BBF89288-7B65-4802-9C92-6C1B5584FE8F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a15ff209d097dc0f73e07370f427fe903764b10d","datavalue":{"value":"7111187","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234717$800166BC-F9AF-4E70-B013-AF7B06A2401B","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":"Q5234717$7D158C03-2481-4695-980C-759B71C3D676","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d008c0652adbb92fc29f999e1cff965654b89fb0","datavalue":{"value":{"entity-type":"item","numeric-id":1917067,"id":"Q1917067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$6B1A30BA-831E-4D71-A29C-AB3883614578","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":"Q5234717$E3B79930-17E9-4887-924A-2E2E409E0116","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":"Q5234717$62212230-F79D-4068-A922-E4AD291A2DB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$157147A6-4DE8-421D-B6BF-8F30C9047AF9","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":"Q5234717$944CE779-6477-4605-9780-BDAFAFD73357","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":"Q5234717$875EF879-2122-43B1-963B-A69B3209DD72","rank":"normal"},{"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":"Q5234717$529F366C-AAE1-4E62-8CE5-5FA4D7D96C85","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":"Q5234717$BBC4C112-18BB-47F5-A357-0F5D6A8DC7F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b48d7b42095141e48a9c1788caedf5498122de8b","datavalue":{"value":{"entity-type":"item","numeric-id":31441,"id":"Q31441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$A704F73D-14D4-4017-9043-1748D755C470","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":"Q5234717$FD30E169-D0A0-4F0D-825A-AE82E4578F2F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ae9e7ed1a239debb49636e759446781c2501e446","datavalue":{"value":"https://doi.org/10.1007/3-540-63104-6_34","type":"string"},"datatype":"url"},"type":"statement","id":"Q5234717$49546DBE-91C1-4027-A5C0-55E4F79EAD10","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7b24be7080e3a9164bee7cdce5cb26dacb431a59","datavalue":{"value":"W1592271195","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5234717$30FDE811-08C2-4C4B-8108-EF7CC65212AB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$BEDE0E2C-5A36-4EFC-870D-31C4E04D03BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"531e66c9bd727d2b988c5a46f114a5b32307e5cc","datavalue":{"value":{"entity-type":"item","numeric-id":1977123,"id":"Q1977123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$AF627DAB-EC25-4AD2-9541-97B829DF3C4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$C25B6AB9-CB60-4790-B11D-EAC23560B9E5","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":"Q5234717$46E8BB2C-9D82-4413-A2AA-5769BF41BCBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65efe90aeec3ecea495173e06d24a23ea70e7b60","datavalue":{"value":{"entity-type":"item","numeric-id":4375633,"id":"Q4375633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$1CB8C45F-351F-4545-9C42-4D34C313EA5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e40c9c557c135eeb7ecb9f55bce2bdb98ea8b63","datavalue":{"value":{"entity-type":"item","numeric-id":1899911,"id":"Q1899911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5234717$A6796747-C909-4B21-9054-B38B17EFECF3","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":"Q5234717$386336AD-2847-45FD-A86A-2C97AF549293","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b7f4e39126d140b1fb7374f494c75cfd56020b6","datavalue":{"value":{"entity-type":"item","numeric-id":4790669,"id":"Q4790669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb1ab665fdf7c6afaa3a1ff2e42ced0c9251b7e4","datavalue":{"value":{"amount":"+0.779958188533783","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":"Q5234717$0F44D0B0-F2C0-488A-B922-34AFAC2A7CC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"542418b998932333df98aeb849260f0e64e3bcdf","datavalue":{"value":{"entity-type":"item","numeric-id":3750136,"id":"Q3750136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa5f2eda90767371b72969e26ea98efe66dc48cf","datavalue":{"value":{"amount":"+0.77599036693573","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":"Q5234717$612477DA-75D7-4A14-9CE8-AD7CFE753ECE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d619869ad0302d9b9fe0d70f22451dd60a21bf06","datavalue":{"value":{"entity-type":"item","numeric-id":2782486,"id":"Q2782486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"73aa20584abb2abfc1351167234cd7a319e20a98","datavalue":{"value":{"amount":"+0.7758384346961975","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":"Q5234717$CA84FB3F-7BA5-442D-98E6-CDF889DDFB2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2740de1b98a7d9aa5a10e33e29be5347f5c1c062","datavalue":{"value":{"entity-type":"item","numeric-id":4375633,"id":"Q4375633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e2963234ede7d99e70ad030fc4d91eac783664a","datavalue":{"value":{"amount":"+0.7511819005012512","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":"Q5234717$9B9299D1-B1E8-4A4A-9F40-4B683D95D268","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f62d3c74f1452c00e4d697b29b4b03afa7c01b35","datavalue":{"value":{"entity-type":"item","numeric-id":865629,"id":"Q865629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6329a36f3973b4bc72f1aa2f1e533dda15ac802a","datavalue":{"value":{"amount":"+0.75090491771698","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":"Q5234717$A20D0E01-AC3F-4EDF-8F4D-4614553EAFC6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Hybrid interactive theorem proving using Nuprl and HOL","badges":[]}}}}}