{"entities":{"Q5495933":{"pageid":7525493,"ns":120,"title":"Item:Q5495933","lastrevid":58590168,"modified":"2026-04-05T21:46:24Z","type":"item","id":"Q5495933","labels":{"en":{"language":"en","value":"Interactive simplifier tracing and debugging in Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6327271"}},"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":"Q5495933$A144ADAB-4969-471D-9318-6E7A436DE8B8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4f5cbc31eef4de75e252180bd54a98e066f14b81","datavalue":{"value":{"text":"Interactive Simplifier Tracing and Debugging in Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5495933$19C4AC7D-9971-4A63-81EA-D69133556F0C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b993545036c1ab4f3d2eb928ed61090f45c1d93a","datavalue":{"value":"1304.68156","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495933$629F9BEE-5F59-4C5A-B849-A7686C126100","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9b5fdf99cae0b3b1aae2662193ea3e7475e78dd5","datavalue":{"value":"10.1007/978-3-319-08434-3_24","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495933$3225A524-557D-42ED-B629-6BBC13A981B3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"883af36fdcd4e56579d2a7dd06af05c0049d023a","datavalue":{"value":{"entity-type":"item","numeric-id":1663227,"id":"Q1663227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$CDC70017-0030-46A8-8108-F85999BE4271","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":"Q5495933$6E7AFC40-B1AF-4280-B610-547D9E1939DE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1c94d745affbb1f035e3911adf053858df897bb7","datavalue":{"value":{"time":"+2014-08-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5495933$7A36FA4A-EBEF-41AE-98A8-40479D2B1404","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7bc40ae685b7f0ba6529ef51e5bfe9c76a7dd47e","datavalue":{"value":"https://arxiv.org/abs/1406.0292","type":"string"},"datatype":"url"},"type":"statement","id":"Q5495933$15938AE0-7C0C-4D80-BBAA-94520B4E5989","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495933$54F25DD4-F6C4-4CD3-B174-1F590DFD0977","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495933$4E86445D-35F9-4858-82F9-DDAA6599464B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8424a111804b8db17d20e330b83c52cf5cad9fbc","datavalue":{"value":"6327271","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495933$AF33C493-3832-4BF3-95ED-24B65607A70B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495933$248F6570-5E3D-4F34-8DD7-E89DB5C5A414","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9171706b2948eb39a15a44f2b1d3f5ee9e220c5","datavalue":{"value":"simplifier","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495933$4812C07B-8A23-4250-89CD-D367F6CCFFBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495933$35FF8655-7BD5-4EFC-B30D-525890A98E8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ccc7af04a2eeabb45dbdd271a70ca2e562240381","datavalue":{"value":"tracing","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495933$4E58C837-4C4C-4410-BFA4-264AA731BB2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e209e27ecbb3fc4e2dfd619db86ffda1231648d6","datavalue":{"value":"debugging","type":"string"},"datatype":"string"},"type":"statement","id":"Q5495933$C9657926-7748-4A56-AEA5-F9E1D218D4BB","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"32d0725c03964dfdedc600d0e862bc44cd0bfc53","datavalue":{"value":"Q57955192","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495933$788D246E-768C-4A03-9D9B-954F137DADD2","rank":"normal"}],"P1463":[{"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":"Q5495933$E99ED853-BBC1-4ACD-B6DB-5081BA777D76","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":"Q5495933$0D369605-BB01-4D80-8CFC-DF0CDC151C72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$C7DFC237-BA16-433A-BA35-0F1330803958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$7B654A8C-CC5F-428A-B7C8-4234E37FC7BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$115FBA1B-B3CC-4783-8C78-0F377739D386","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c79e7ab23ee82c98546ee8c91c30e7af9df0ec50","datavalue":{"value":{"entity-type":"item","numeric-id":21882,"id":"Q21882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$2B069001-AD03-44B5-97DE-AE82A2586978","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":"Q5495933$50151818-5FBE-4639-983F-13B8A3AF1A7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0aae91b3cebe1e84c9813205ff5ebc7d8b0f6804","datavalue":{"value":{"entity-type":"item","numeric-id":18521,"id":"Q18521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$373E688F-F36E-495F-9BEB-7E9B5CB5846D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f3dc49212bb1ac953b456b7ee6d37c17258b97b9","datavalue":{"value":{"entity-type":"item","numeric-id":18543,"id":"Q18543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$B554DA65-96CC-4752-8258-A638CE025F01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"68a02c8b1ab8ed182d6b6b861d09c8de6f71d04c","datavalue":{"value":{"entity-type":"item","numeric-id":21661,"id":"Q21661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$18E26324-9832-4533-A240-5460F4FD758A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8820312195fedfa211b44ae20ae12e4a82ec2682","datavalue":{"value":{"entity-type":"item","numeric-id":23299,"id":"Q23299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$A276EA9E-0A61-4D59-9224-2D9D5D0E1E9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e05716d11354c9d38e76a1ec25809265e02d101d","datavalue":{"value":{"entity-type":"item","numeric-id":24961,"id":"Q24961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$C8C2FF74-B668-485E-A149-09DAD3F0269D","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":"Q5495933$6F0E8E81-46F6-4D57-A229-90F213E8384C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5e90bd29d5a42ad58f37e27960341df9d1554318","datavalue":{"value":"W3102762027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5495933$4392947C-C03C-4EF9-B3F6-1620F7A8C3CD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1196f5e17dff99bc1a9d16ec3c58ef966832597d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$D5F549DA-2FB7-4B4C-9095-764AE2B573A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad5469f72b3d14e0a040a00af8c98b8e5cf4cb2b","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$613302B9-1088-46BC-A85F-C40ADE4E958A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58140cb8afbfd1e28d381fbe9968bc9f5b2e9afd","datavalue":{"value":{"entity-type":"item","numeric-id":4222853,"id":"Q4222853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$2FEFCEAD-45E9-43CF-822A-1C0830DD1BBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99d32070e79ce8a8454df29df688e840bc5b6a18","datavalue":{"value":{"entity-type":"item","numeric-id":4423202,"id":"Q4423202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$08B5D1D8-33CE-4061-BB4A-9AC0B6E56DEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f342ea4f6edcfa9b24e8c4722a1d0f43147ce5a5","datavalue":{"value":{"entity-type":"item","numeric-id":4844167,"id":"Q4844167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$156DABBD-3D56-4E8C-8BC8-CC89FA77C344","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed22a42a8ed35e56391b6c3d008af8d8059adf6a","datavalue":{"value":{"entity-type":"item","numeric-id":5170238,"id":"Q5170238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$0C5795A9-BAE9-48F6-8B59-0F9B6EDA4074","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07d763717b639e10adfdb52f6d0aed821444ad5f","datavalue":{"value":{"entity-type":"item","numeric-id":2907353,"id":"Q2907353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5495933$E2F671FF-B6CA-471B-A8FE-F0146F78CC11","rank":"normal"}],"P1643":[{"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":"7a85ce5e4de4d7aed8c526c3dff22ebdb69f2c22","datavalue":{"value":{"amount":"+0.7242708206176758","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":"Q5495933$EF3A29A5-A00E-4FB2-A802-FB2AAE786D52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38394b4e8d3a3502630a463829cd1f4840ac5524","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"233f89ad5ad55e1f0e187814aa2778e4637d4d57","datavalue":{"value":{"amount":"+0.7169886827468872","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":"Q5495933$14787AD0-60BD-4838-A6D0-E68B519A70D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b18f1bcee5a559e76e86ee84dd5601244af54f6","datavalue":{"value":{"entity-type":"item","numeric-id":909488,"id":"Q909488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ccb1ce4793519f0625bdbf18ef60486fb7836df","datavalue":{"value":{"amount":"+0.7099419236183167","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":"Q5495933$0B4BD4C4-3A0B-4961-B04B-693299DC62E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef914c5d16ae991870856bd539a5283395a477b7","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ced16ddac369cfc0077c14e67003bce26ca5f1a","datavalue":{"value":{"amount":"+0.705674946308136","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":"Q5495933$B55AA8B4-0F05-40AD-A18B-E6A61C250531","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9bfe76c583713b55eadf25fa3d88d354ebc06b63","datavalue":{"value":{"entity-type":"item","numeric-id":2879273,"id":"Q2879273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42716e35e14d52316126eb5e1aa2359ef365fc58","datavalue":{"value":{"amount":"+0.7019245624542236","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":"Q5495933$2DEBDFC8-6F4C-44DF-A53B-1B45E5EE45C2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5495933","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5495933"}}}}}