{"entities":{"Q4993363":{"pageid":7022940,"ns":120,"title":"Item:Q4993363","lastrevid":54021902,"modified":"2026-01-26T02:51:27Z","type":"item","id":"Q4993363","labels":{"en":{"language":"en","value":"ProTeM: a proof term manipulator (system description)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7359427"}},"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":"Q4993363$B215C17D-FDF2-4BB2-965E-6BAA55B6072E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f8dbedead02e01d6f2a1196aea6e595f0dc4a714","datavalue":{"value":"1462.68218","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993363$AEFE0917-8B37-4937-93BD-3A5C09E80A52","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9866063e90575cce23c54d43ac46a7ebdaa56f4b","datavalue":{"value":{"entity-type":"item","numeric-id":2305424,"id":"Q2305424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$43660194-CCB7-4510-A0CB-A2BF37340443","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7072b29ec05013e9a2e81e1795de7757de4265ff","datavalue":{"value":{"entity-type":"item","numeric-id":293293,"id":"Q293293"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$9F2839ED-40AA-4442-A5C7-EA8BE6119A4D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19226134edc7102663c447aa756e808a7a8d2948","datavalue":{"value":{"time":"+2021-06-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4993363$C02D5760-6BF1-45C2-BA85-AEB713B8D24B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993363$47994299-0F85-4061-84BE-4BCD5F0BCF99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993363$E6AFCE2C-96E4-4C76-9C28-EA981A580AB9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6982d0ca70ca2afff3a4a6c39d4b18765c7eb597","datavalue":{"value":"7359427","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993363$F7D5B43E-4E55-4421-B005-9D9B2DACBF43","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e1f66f838ab6c659c40577faeda90140c2435bc","datavalue":{"value":"proof terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993363$244BBB7B-5588-4800-8203-98CC52CEA10C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993363$1E425D3B-881D-40EB-9846-774CD2F009B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a47f70748fcccf1129411fab33092ea7c740559","datavalue":{"value":"interactive tool","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993363$4A58D5F2-B22D-4AE2-ADA4-0C213C3BA25E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9f397c52f37228d72babea7f4da967604853d803","datavalue":{"value":{"entity-type":"item","numeric-id":22077,"id":"Q22077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$E5020088-1699-4A81-B303-11465BF90CD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0e6be5cef030e1f0832b2f49829505d385eacd56","datavalue":{"value":{"entity-type":"item","numeric-id":44022,"id":"Q44022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$0BC015D4-6777-4D45-B796-7EE99C9B307E","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":"Q4993363$B9F7A957-B0EF-42F5-AB25-4319E7AA1276","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"90c227478d93e0b870e0c78c09c2776f3a08c57d","datavalue":{"value":{"entity-type":"item","numeric-id":438562,"id":"Q438562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$753DAEB6-A466-427B-AC62-FCB2630965C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"599c5dbf52817fbbe5f2f15e33a96dc6ac97514e","datavalue":{"value":{"entity-type":"item","numeric-id":3908463,"id":"Q3908463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$5B9E2ACF-3863-4B14-9E5F-41F485C09331","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9e2338b7c806b48af5129c7f0771362df0f7c3f","datavalue":{"value":{"entity-type":"item","numeric-id":5170824,"id":"Q5170824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$89FBBCF9-F0CF-4307-B088-4AF836D56399","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec728f31448e01ff9e5cfe09b4a0aabd5ac40247","datavalue":{"value":{"entity-type":"item","numeric-id":2829264,"id":"Q2829264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$5537F21C-B8B7-4B8D-AA2F-19D9025392E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4cc846e4285dd73747ab89d2dd8d67254289009","datavalue":{"value":{"entity-type":"item","numeric-id":4799892,"id":"Q4799892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$0C88EFD1-7407-4817-B72E-47783B784F7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e4935ad48e4266d08c483ec2131b1e0a201050d","datavalue":{"value":{"entity-type":"item","numeric-id":1392147,"id":"Q1392147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$4D37D68D-9223-4340-87C5-554EC4056281","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60207ca25bfa758b9590cffdf67a8ee6ad2806da","datavalue":{"value":{"entity-type":"item","numeric-id":2843602,"id":"Q2843602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993363$15138452-73CF-4366-B0F0-3A7B228FC00E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bb89a312289fdd64537dfe22ed150d86dc30dae2","datavalue":{"value":"10.4230/LIPICS.FSCD.2018.31","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993363$F7EB2F86-9FAD-4382-B6A4-6BD9D99D2044","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e7c6885db120465d3fc977ee01677784fd7b685","datavalue":{"value":{"entity-type":"item","numeric-id":3809309,"id":"Q3809309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"324bf3c8f4df6773d10c234b4999c6681f86e038","datavalue":{"value":{"amount":"+0.7648782730102539","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":"Q4993363$87F70930-93B3-41C4-BD33-AAF641150C68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9796d7520d7b11fc49e48598e4e7c8921bdf8142","datavalue":{"value":{"entity-type":"item","numeric-id":2841249,"id":"Q2841249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"443ac519c4961e4cfa9269656abc0c55907c7296","datavalue":{"value":{"amount":"+0.7638342976570129","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":"Q4993363$83FC18DD-2ED6-442A-A137-4FD878C0BF3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd3366842136fc5098da90336de187648cc4944b","datavalue":{"value":{"entity-type":"item","numeric-id":876042,"id":"Q876042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23b9f6ddbffa7a64019d89023d1aa182a1784fee","datavalue":{"value":{"amount":"+0.745286762714386","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":"Q4993363$E003D27B-F8B7-4E09-8E87-D01C79FE0E71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30efdf4a0482619b878c35fc5f95adabcdb9e2bc","datavalue":{"value":{"entity-type":"item","numeric-id":4447241,"id":"Q4447241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"296cb9625d81f548ce77ee9e42fe2e8402c089cd","datavalue":{"value":{"amount":"+0.744408905506134","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":"Q4993363$99E2157D-8F59-4077-B808-45D3F02B9BAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21035bcb7504aecf5f37020f49f00765792a69b3","datavalue":{"value":{"entity-type":"item","numeric-id":3680267,"id":"Q3680267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a89cfa1c1931b3d149cb1e6bb7c0840b4d0d67b4","datavalue":{"value":{"amount":"+0.7439038157463074","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":"Q4993363$F34720CF-2264-4D2B-BE5A-629AA3DE2AAA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4993363","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4993363"}}}}}