{"entities":{"Q2305425":{"pageid":2316168,"ns":120,"title":"Item:Q2305425","lastrevid":78459821,"modified":"2026-05-06T11:38:46Z","type":"item","id":"Q2305425","labels":{"en":{"language":"en","value":"Composing proof terms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7178985"}},"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":"Q2305425$A83F5472-1F23-4CAE-90EA-502294D6A4A0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"71554ae194dc3f0862670bd5c6a9683adff5ed27","datavalue":{"value":{"text":"Composing proof terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2305425$497B28BA-FD9C-4D44-9FED-986245D0022F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"86305ed516185d21744d114c0aea16077d8f601b","datavalue":{"value":"10.1007/978-3-030-29436-6_20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2305425$DE95B6C5-EE3C-4247-9804-C3FFDF4A5C71","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":"Q2305425$50601B59-FDFD-4D1D-9111-4EB51C1D7455","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":"Q2305425$450DC978-4519-4A89-B475-3F1BB4612E01","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9cf314df552e26dc257d6d24b288f7144e19fa20","datavalue":{"value":{"time":"+2020-03-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2305425$4600C0DC-44DD-42F4-AD23-892EBEA5FCB0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2305425$1F34AF15-317E-4727-9E88-78A3E00D5292","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2305425$DBDE6DD9-F1BB-4C5B-B168-838E3238E680","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"423d4f1a032740e4698a74b8b8d0e502b36b03c0","datavalue":{"value":"7178985","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2305425$C6157E57-F303-4A46-86DF-F2AE948C96DE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e1f66f838ab6c659c40577faeda90140c2435bc","datavalue":{"value":"proof terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q2305425$A0EF40E7-38EE-491E-A352-9D4601440902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q2305425$D85A2396-9B29-4DAB-915C-988ACCAD7DFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7010e5ebaf593fc81efbecd62427d5100a588a3","datavalue":{"value":"automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2305425$444A4B89-1B23-4B5E-861E-65DBA902B7BD","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":"Q2305425$04F694E1-5E18-4500-A00E-9EF5EF9D20CE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a95677992ffa90650f8c9b53e8eb2912d96c1ec4","datavalue":{"value":"https://doi.org/10.1007/978-3-030-29436-6_20","type":"string"},"datatype":"url"},"type":"statement","id":"Q2305425$F7754DB8-9F66-46B1-8627-719FC746C6D7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c645ef452cf8d0fced00d191594a27606e9c477f","datavalue":{"value":"W2969720931","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2305425$0DC0F147-F189-45C5-B776-5F29CACC5F63","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2305425$4C589D44-4678-4480-AE43-9B0D8A2A354A","rank":"normal"},{"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":"Q2305425$E8BC690F-B495-45ED-86A7-41F120CF90B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95ea95e27a0d26a4df4db00149bde9cdca6bbb6a","datavalue":{"value":{"entity-type":"item","numeric-id":4993363,"id":"Q4993363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2305425$FB2AB593-A3AF-498C-9B33-DD2A698B1274","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"720f52ab783e3305f6a4289711e5737a68051525","datavalue":{"value":{"entity-type":"item","numeric-id":1615001,"id":"Q1615001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2305425$CD31D0BC-9BA4-4FD1-B2BC-8F33F88DFBC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c264d0378a5f30df399a3e5c6ab315df59ddacaa","datavalue":{"value":{"entity-type":"item","numeric-id":1190488,"id":"Q1190488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2305425$06A583EB-9583-4D9F-9709-6B20F9E14CF0","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":"Q2305425$58AA6821-74FD-4632-9100-549268BD1BE2","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":"Q2305425$D2C8B6F8-1482-449C-8397-EA7B8AD13AD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c17bfb483d5172a78bdd7b00d1ae9a46a60c3539","datavalue":{"value":{"entity-type":"item","numeric-id":4847000,"id":"Q4847000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2305425$1EF5F4C2-029F-419A-8FA8-E0B4824EE040","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66e219b98f078c7b1c784369ec991d66227b6d06","datavalue":{"value":{"entity-type":"item","numeric-id":4993363,"id":"Q4993363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eee549bce70a3c0be71969e5016f6ef6210775ff","datavalue":{"value":{"amount":"+0.8106536269187927","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":"Q2305425$6CE9CBDD-3E96-48BA-B72B-0BCB97344247","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9784fc600fb67b4b96830236fce75733ee5e9714","datavalue":{"value":{"entity-type":"item","numeric-id":5170824,"id":"Q5170824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce21b589ed83e93897ff0ca7ab2211be4cc59349","datavalue":{"value":{"amount":"+0.7608440518379211","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":"Q2305425$5C4B9A37-3A13-49E9-BEA1-D04CCC4796B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ecdeee46e504a55acd7bccfff46c1219fa96e652","datavalue":{"value":{"entity-type":"item","numeric-id":4842538,"id":"Q4842538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fce7469e44fffa7cf3031c63ca9faa2076fc9f0a","datavalue":{"value":{"amount":"+0.7398684620857239","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":"Q2305425$75E1DA74-2D1B-4E97-9C87-F06AC0865E89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f30c460421c2fa6f05c5890bcf39b2153618542","datavalue":{"value":{"entity-type":"item","numeric-id":5055865,"id":"Q5055865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f89030f1bee9454c64cee85ad4305f76f47c88df","datavalue":{"value":{"amount":"+0.7332409620285034","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":"Q2305425$A01C14C3-B9BB-4CEA-A2C4-D490053932A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38df53b8605541130f67bf0b0610f7190a947415","datavalue":{"value":{"entity-type":"item","numeric-id":2424890,"id":"Q2424890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f98c0a9865fa455dc7355b87b2d70a04ec548ee0","datavalue":{"value":{"amount":"+0.7321898341178894","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":"Q2305425$C041BAFB-4B29-4790-BDBB-9B9C9711C3CD","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2305425$B77184A2-BABB-4853-AA35-54DE030A9AAC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Composing proof terms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Composing_proof_terms"}}}}}