{"entities":{"Q1687709":{"pageid":1698450,"ns":120,"title":"Item:Q1687709","lastrevid":71999583,"modified":"2026-04-14T01:59:28Z","type":"item","id":"Q1687709","labels":{"en":{"language":"en","value":"Automated theory exploration for interactive theorem proving: an introduction to the Hipster system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6821840"}},"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":"Q1687709$CDA3A957-0059-4A27-8496-FA255159D907","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"92cca8d5d7919b5d4baf647206c4e848d5862ca5","datavalue":{"value":{"text":"Automated theory exploration for interactive theorem proving: an introduction to the Hipster system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1687709$5BA615AB-90D9-4590-8A7C-5A336D1FAEF6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aa8ffd2d07d82acc1bc3c52fdbee19f0337f39cc","datavalue":{"value":"1483.68484","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687709$3B8CABF2-524A-43B5-B0DB-968D69844FA3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f1fe77b4a8aaadaa57a239747b5d5c70f1431dd7","datavalue":{"value":"10.1007/978-3-319-66107-0_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687709$644880D4-8D1D-4EFE-AD61-385138F56DDE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0ff9a748cd6fc1ff0926984ae3ee01554f12fa14","datavalue":{"value":{"entity-type":"item","numeric-id":287274,"id":"Q287274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$5FB13AA2-DB97-406A-B5E6-6B716C7C9A0E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7600255b4ee907c1b1dfbc5f62c7b1165ab1b6d0","datavalue":{"value":{"time":"+2018-01-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1687709$24825B6D-D8C7-4AC5-89BC-8F28C4A848C1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687709$3615A032-6E49-4A52-B7D2-159ECEDDBA7C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"adfd6873a6b0d3bbf61df341bf99e9cccdffcd50","datavalue":{"value":"6821840","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687709$F6DBD941-A386-400E-AFAB-F2D60A35F0F1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$0820C04D-3ED8-4DA4-BC64-F7E3DC8893EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$6500CC01-AFEC-44A5-82B6-18C112B363EC","rank":"normal"},{"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":"Q1687709$49E01F15-6624-411C-9B2A-DD9285759AD8","rank":"normal"},{"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":"Q1687709$6A9A1D38-77B9-4A32-A1CA-37C8FEC6BC4D","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":"Q1687709$F0484BCE-CF18-4F5A-A261-82AB5CF4DFBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$020E98B8-1000-4D27-9C72-CFC980C25A5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$164D6E9E-47CF-4D69-9206-DD5EC5FACCA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6a5699a860dd7dc9c732976be3ba437fb61ff7dd","datavalue":{"value":{"entity-type":"item","numeric-id":19322,"id":"Q19322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$F9BC809C-10A1-462F-AA50-363224A0C9C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$7249797E-89A2-4E2B-8D0D-F3289AF1AAA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"502a85214a09d04d17109076bbc11ff1d79af821","datavalue":{"value":{"entity-type":"item","numeric-id":31034,"id":"Q31034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$91EF37FB-D1F5-47F4-B4BC-5FC3C332B136","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":"Q1687709$5EB73CC2-0DFA-4853-89B5-5E8BD13BF710","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b0ee62efdcbae6f13a3dbdd935d3497b4100e250","datavalue":{"value":"https://doi.org/10.1007/978-3-319-66107-0_1","type":"string"},"datatype":"url"},"type":"statement","id":"Q1687709$4C47BCD2-DD10-4747-9856-7B9B772D80BE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4e6e33195f621b03a99f78af25fdab069e432ebc","datavalue":{"value":"W2758276286","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687709$487031AE-E932-43D0-A2BC-23AF899343A9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"891b68750ed32518a9a712f13cb431304bad6b82","datavalue":{"value":{"entity-type":"item","numeric-id":4780208,"id":"Q4780208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$D6D104A4-428A-4CA8-9D97-B2F4CB208FBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7e013849775846918727fac3e7e6455bd448813","datavalue":{"value":{"entity-type":"item","numeric-id":865646,"id":"Q865646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$B8EE5CCF-76E4-48BB-9FDE-9E3E99A242FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4097ecb980e2df6f5072c854a7151168d79b8bf6","datavalue":{"value":{"entity-type":"item","numeric-id":4928454,"id":"Q4928454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$40569178-671F-4122-8840-B4811E2056F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"898d2836e77c209a26cdc90309154e79d6e4a365","datavalue":{"value":{"entity-type":"item","numeric-id":3453129,"id":"Q3453129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$56E8759A-6FFA-4AF7-B51F-02C4DAB80370","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc68d0c63fc526ea5871bf3910e143d716cf06f9","datavalue":{"value":{"entity-type":"item","numeric-id":438543,"id":"Q438543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$12B6277A-2291-47C4-9BA2-D117E9CECE86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0933abcee6e71217a619391222ae8646b0eea736","datavalue":{"value":{"entity-type":"item","numeric-id":5495917,"id":"Q5495917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$1970FFD6-03F7-47E5-BDB6-34A883818527","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"206cdc70bbe3c338e895b7600b5aaf2ef6f7c9b7","datavalue":{"value":{"entity-type":"item","numeric-id":2852039,"id":"Q2852039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$A9569C37-8383-425C-8FB5-3EFCC0859177","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$CB24BBB0-9F89-4AC8-B1F1-6C9B98BD0309","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4722d0b626fc70eb1b4335a052138c3c2d6c3820","datavalue":{"value":{"entity-type":"item","numeric-id":3460056,"id":"Q3460056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$4F325A48-5A54-45FE-B3F2-0B49B4A3831F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f927eef2ff97bc2ae67635a63548bc51b9896f2b","datavalue":{"value":{"entity-type":"item","numeric-id":5371995,"id":"Q5371995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$24F3C7BA-6666-433A-A2FD-D09AB6BC873C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687709$4E3570BB-D284-4ADF-8C50-040BA89D4AB2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2f7f034221b4fe3cf9cd1ad0e17d3f6f5ecbbd2b","datavalue":{"value":{"entity-type":"item","numeric-id":5495917,"id":"Q5495917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12dab623f830a696acd9704bb9a2350711b26967","datavalue":{"value":{"amount":"+0.9190306067466736","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":"Q1687709$155F147E-B6E8-4C67-A08E-522F26C0230A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51fcff8cc9dbcb717a672d7a1551323231e5d33e","datavalue":{"value":{"entity-type":"item","numeric-id":6108814,"id":"Q6108814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c6d95c62f26af3bde2ba6ceec67ca33e3abe546","datavalue":{"value":{"amount":"+0.8371188640594482","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":"Q1687709$93335F2E-4090-4022-92BD-AB574727E465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a8b950c83128d11d71296f04dbe09c8f568420f","datavalue":{"value":{"entity-type":"item","numeric-id":4928454,"id":"Q4928454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"235395832042503e7cfe3e239de7684267308d21","datavalue":{"value":{"amount":"+0.8256587386131287","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":"Q1687709$7AC0B732-8786-4EF6-B2D3-FF8BDD2654E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dfa61574fc575acc4cb7d0ca05a72ef1b08a526","datavalue":{"value":{"entity-type":"item","numeric-id":2287904,"id":"Q2287904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"314e839b69ec35a892d38d1ced83b16b8cf3fbd6","datavalue":{"value":{"amount":"+0.7814878821372986","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":"Q1687709$F4AEC009-9AD9-4645-BCDF-F928C62E37DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"88afd69a9b242c093828197147a90fd80978ffa3","datavalue":{"value":{"entity-type":"item","numeric-id":4499159,"id":"Q4499159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"645604e7acaa83dc5629b40f88d6443cb2ff335f","datavalue":{"value":{"amount":"+0.7706969976425171","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":"Q1687709$33B35419-2C4A-4401-887E-3EC88F8FA82C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated theory exploration for interactive theorem proving: an introduction to the Hipster system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_theory_exploration_for_interactive_theorem_proving:_an_introduction_to_the_Hipster_system"}}}}}