{"entities":{"Q2819200":{"pageid":2829938,"ns":120,"title":"Item:Q2819200","lastrevid":83690705,"modified":"2026-05-07T09:59:28Z","type":"item","id":"Q2819200","labels":{"en":{"language":"en","value":"Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6630643"}},"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":"Q2819200$4442AA03-DF04-481E-8136-BF55E52B920B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"323f5ddde0d3e6ac685917cbeb89c7a973c7cf38","datavalue":{"value":{"text":"Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2819200$110AB941-0FFD-4F0A-B4A2-5D972FE7AED4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ab9adf27d632920592974ae96b2e4d9e0ddb4e88","datavalue":{"value":"1434.68641","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819200$826785E6-C4A0-4843-80D9-1B1364BF9FFB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5397856525449395bcbe31c5f12ad3ebe89d9cff","datavalue":{"value":"10.1007/978-3-319-42432-3_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819200$C60A6FE8-B808-479D-850A-21F820199B8D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"89aeebbd519907b23fa0a230e61b08e676dd99f3","datavalue":{"value":{"entity-type":"item","numeric-id":1798966,"id":"Q1798966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819200$28A9BDC4-63CE-4F90-816D-E3162BF49C7E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"5ce1d49245d97a30ecabe94a0469a6616f4841aa","datavalue":{"value":{"entity-type":"item","numeric-id":2819192,"id":"Q2819192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819200$3389CBD3-D162-4030-8FAE-F28B36C3749A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"300772c5a0b58bf4f4bfdafa9010450cf2acf8fe","datavalue":{"value":{"time":"+2016-09-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2819200$A756BEC1-C9AF-47CA-BF15-A01F8E337C95","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819200$D2977705-27F4-42B0-94E6-2B74D2A7FCBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"173b0c3afec7c4f9f987722665cc7bdb6b8f5813","datavalue":{"value":"13P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819200$C55917BE-904F-4C62-9303-E7AAD7C393D3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"843d56ee33be9a2e19bbc159fd6f4b9fcad248ea","datavalue":{"value":"6630643","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819200$AD0FFBEE-1EC5-4716-99B0-EFACA4C4ACE9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a00b2c38dcbf66a9ee3b6ec267b130b3df1e2b3","datavalue":{"value":"computer-assisted mathematical theory exploration","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819200$72D14482-6BE2-4BF2-B7C4-606BD4D57573","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819200$6B767123-AF24-4FAA-A00D-9B8D2D5E4145","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"37db48fc50878deb5298f058e27a669b8c15ab38","datavalue":{"value":"Theorema","type":"string"},"datatype":"string"},"type":"statement","id":"Q2819200$EB45F854-AA67-4529-87EC-99FCD183A5C0","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":"Q2819200$121C771E-5087-4919-8204-A367542D0075","rank":"normal"},{"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":"Q2819200$C2B2028F-0F29-4BB1-A139-E897CE37C947","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819200$34EB4F07-FB45-4244-A3D5-12D583159C2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819200$527DE8DF-2EB5-4B79-92E3-A77FF550F59F","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":"Q2819200$48EF8234-3CE5-4EC1-8F96-9FA817B4DAFF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"14212db3e7afb6cf0f19a551a78762dfa83e0459","datavalue":{"value":"https://doi.org/10.1007/978-3-319-42432-3_8","type":"string"},"datatype":"url"},"type":"statement","id":"Q2819200$A70FA83A-44CF-4187-BA18-D174D970B67B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c8fb7a27116bf7fb2bac730bbc6f739d51994fa5","datavalue":{"value":"W2495091588","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2819200$34D19808-69AA-4B07-ACF9-44002F6817FC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"879ff0fb88210b640562cf6d40b040cd31a37674","datavalue":{"value":{"entity-type":"item","numeric-id":2817288,"id":"Q2817288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819200$472D78BC-3209-49A0-9FEE-6D9E31AE210F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"148fa272dfd5b3538fd0793ae331434241fdb821","datavalue":{"value":{"entity-type":"item","numeric-id":5387844,"id":"Q5387844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819200$1128C65B-00F1-45D6-AAA0-BD86364DE4BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"169b2f339340359af747448063c133ed6019c736","datavalue":{"value":{"entity-type":"item","numeric-id":3395096,"id":"Q3395096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2819200$ED145725-E028-44EC-9928-80ACB8FA6CC1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a3c074ee182c14fb829f48d8ee3067fb50232e8","datavalue":{"value":{"entity-type":"item","numeric-id":3336730,"id":"Q3336730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27eb9e233eb8dfbe57a0a3e44bacfebb20216e69","datavalue":{"value":{"amount":"+0.9152473","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":"Q2819200$1A9AA7B7-C2BC-46B5-9CA5-6B20DE92D633","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a02b2bfea1c5f47cd601f5ce8d9525ee86d87fe","datavalue":{"value":{"entity-type":"item","numeric-id":5219926,"id":"Q5219926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8027d47798c6cf274fd49803e839ac85526e960a","datavalue":{"value":{"amount":"+0.90744966","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":"Q2819200$524B8055-B6F9-4E30-A705-72D91B89E8C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b334918dd1a2aa0f0f022268f87ecb12c10c047","datavalue":{"value":{"entity-type":"item","numeric-id":2881098,"id":"Q2881098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1804a798f8a42d2f8ad2f769cde5d35d82e45611","datavalue":{"value":{"amount":"+0.9054544","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":"Q2819200$D440C34C-C66B-43C3-82B2-90C2EE59D407","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a936d133626ea4aea0632a5ece76b255664803e","datavalue":{"value":{"entity-type":"item","numeric-id":287356,"id":"Q287356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9945e9629129deb125fc5c8da3af1eb56402f3bb","datavalue":{"value":{"amount":"+0.897727","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":"Q2819200$79819B39-9487-4748-91CC-F58103317A33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5a66faa01dbce681557a69b916ebefc9578b7e4","datavalue":{"value":{"entity-type":"item","numeric-id":6173578,"id":"Q6173578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2cef1eab210fcdd10f5d6be20756cfd768ca3513","datavalue":{"value":{"amount":"+0.8962878","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":"Q2819200$513C428E-04D1-44B7-A3D3-1BFD9369B05D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0c53ff24d99dc5823b47104c19e4145b1541675","datavalue":{"value":{"entity-type":"item","numeric-id":688727,"id":"Q688727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f071b770df62b2be4566494c28a18f416a238d4","datavalue":{"value":{"amount":"+0.8935988","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":"Q2819200$B34EA8C0-4046-4EFC-9FAC-C1BF174F124B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fbbad55ea327bd2b71a72261e8db306a544d6454","datavalue":{"value":{"entity-type":"item","numeric-id":3021903,"id":"Q3021903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f932db08e28d1234aaaed2dfc0cbec3ac9b9270","datavalue":{"value":{"amount":"+0.8927936","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":"Q2819200$23F39F1A-F786-4E1F-91C6-7ABCBF0B7854","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9309577822db3b21e2b3a967403d44aa61bb595b","datavalue":{"value":{"entity-type":"item","numeric-id":5387844,"id":"Q5387844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88283ca9490ed27ca2e2a639667f15eff88ec6d9","datavalue":{"value":{"amount":"+0.8910844","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":"Q2819200$2B77A41D-3B61-420B-8C16-8B24212F1CFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"832adab52a6be03c508c7df724145ae73e85a03e","datavalue":{"value":{"entity-type":"item","numeric-id":4524768,"id":"Q4524768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"17b7f0c88c6151ccf073c591ad9e43ae47801b6f","datavalue":{"value":{"amount":"+0.8893584","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":"Q2819200$3FC95354-0037-4BC2-AA27-15464D45C7F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"116ae40af25df1caab31ce7865056cc8623f9e19","datavalue":{"value":{"entity-type":"item","numeric-id":3789101,"id":"Q3789101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0083dfcf8fd1d4b60753033f4c024c1dbd6ff7f","datavalue":{"value":{"amount":"+0.88867486","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":"Q2819200$AC5759C3-45CA-4176-A6E9-9BAB6BB5F04E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Interactive_Proving,_Higher-Order_Rewriting,_and_Theory_Analysis_in_Theorema_2.0"}}}}}