{"entities":{"Q5919012":{"pageid":8050210,"ns":120,"title":"Item:Q5919012","lastrevid":93437738,"modified":"2026-06-05T04:23:58Z","type":"item","id":"Q5919012","labels":{"en":{"language":"en","value":"Constructive decision via redundancy-free proof-search"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7268899"}},"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":"Q5919012$1390E0F1-EC16-4FD7-9835-FF59BA766887","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"55ee5de75f7ad49b6c895f0d0b3880ff94557f10","datavalue":{"value":{"text":"Constructive decision via redundancy-free proof-search","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5919012$DF1FC1DE-A54A-48AE-92E5-0C4DD653D882","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9906d1f082efff529f2fb215fcb6d0492ff42771","datavalue":{"value":"1468.03015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$054E436E-3231-4726-A276-BED5321E3FB7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa467ab0fb5921a8aef55b984db7a2882bc4957f","datavalue":{"value":{"entity-type":"item","numeric-id":877885,"id":"Q877885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$865D6879-DF78-40E0-B459-63152FB5575A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$B41CFA99-5806-4DE8-A3C3-ADB6B4AA99C4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4011c0437b0c50916bbdc1f2b0514a4c041c71e0","datavalue":{"value":{"time":"+2020-11-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5919012$2B5869A1-0B03-4598-955E-386AAFCA91F9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$519A3CD3-20BB-4265-8504-302336221B6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$57202FFB-EF81-422E-809F-5F8D7E51CFB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$032614B1-AB76-4CA1-92D0-15C4FE17D0AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$AFCFFB41-A917-4A7E-BF6A-17D699C4DE2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$10B55FBA-CBD0-4B01-B559-82BD38797394","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fb30d36c699797ce8e1a0e31a2fdbf067b56b2e8","datavalue":{"value":"7268899","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$05663B72-EBA7-40B4-9AF9-681683EA352F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4c8e8f309ee6107ff7c08672be9f1d9a9cacb6bd","datavalue":{"value":"constructive decidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919012$B95CE3D3-B2A9-4D24-A012-34A350B53FB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ce4feea89835b46b1433881e67cdd6f181cb49b8","datavalue":{"value":"relevance logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919012$0E7FBE95-0406-463E-B14A-4D58A9573037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"404e591614190488419156400105486d83841bbf","datavalue":{"value":"sequent calculi","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919012$88FE8000-C5CC-4AAF-92B8-685654F36874","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dbadd689afdff7de47d6fc9658b887b8542f7df4","datavalue":{"value":"contraction rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919012$E5283EB6-F9A0-42A8-994F-8E0657B4FF64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"293765ee67aa9951e05650c40963403f89fef1ad","datavalue":{"value":"redundancy-free search","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919012$86517C0A-3B0B-4836-B337-02D310D7705E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5930e8b62f0ce86a1dfbd0d9b94da4380ec90b98","datavalue":{"value":"almost full relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919012$033F9C82-0D5F-49E9-931E-86233CC3B44F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0a802534e5a1505ddb8dfdf099680e152422fcb4","datavalue":{"value":"mechanization in Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5919012$8EBC13AE-5465-40C6-AAFF-4AB5CF987E76","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$ACC6D749-EDDB-4329-9D30-971AA870E283","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":"Q5919012$68ECF269-96BB-446C-AF5D-AAFB805814FF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"31cedf84e7387b58bc788d6cc5430e0f4bf84de9","datavalue":{"value":"https://doi.org/10.1007/s10817-020-09555-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q5919012$10E342BA-CD14-4A19-8262-2BFC58EF1A01","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"04766aae25852d4485d44e3c1258528c9686e997","datavalue":{"value":"W4205994606","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$5EFBA5E2-BBBF-405B-8455-FEE46E9D930E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e59426938774367af27e2001a2ab42f831578456","datavalue":{"value":{"entity-type":"item","numeric-id":2517231,"id":"Q2517231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$B38A2117-9609-4C94-93D8-C69236A3FB18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3740790bcafb5be42b63a2da2ae21979b744ba73","datavalue":{"value":{"entity-type":"item","numeric-id":4916555,"id":"Q4916555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$29735297-6CBF-4B49-B98E-2093FAEDD224","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc05194544eae6a9c6b3aeaf04f8ad8716f625ee","datavalue":{"value":{"entity-type":"item","numeric-id":4282577,"id":"Q4282577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$9273F51A-CB41-414F-A37C-51A5A31D6C71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05bda265395f5c65b4fa8a0061b4ef96facef65d","datavalue":{"value":{"entity-type":"item","numeric-id":4594260,"id":"Q4594260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$107BBB96-6C0C-4E5A-BF08-456B7C7C58F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"932ebb8a2d35fa5cff618456d5658b9a86184b54","datavalue":{"value":{"entity-type":"item","numeric-id":1694477,"id":"Q1694477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$CB7232B2-D9F3-4242-A8A2-FD8C0C7C1029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6b18d4fc60a70c27ea7b62beac0a6f5c90f6df2","datavalue":{"value":{"entity-type":"item","numeric-id":1936244,"id":"Q1936244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$1FCAAD7F-B5A6-4C5D-8EDA-CBBAC60595EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71ea90137e7a6ebf5cae03c80f9e832796cfc4e2","datavalue":{"value":{"entity-type":"item","numeric-id":5111451,"id":"Q5111451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$17920658-C207-40D1-8888-BC068CEFA234","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494bc5c3e6f65c5794987c5813970bb3adaab9a7","datavalue":{"value":{"entity-type":"item","numeric-id":4944852,"id":"Q4944852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$5083FDD4-75A3-48E4-9E30-182FD1F78F41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ab411898e21b7ff1dd2c5306da3bb87a5aa3f33","datavalue":{"value":{"entity-type":"item","numeric-id":3371525,"id":"Q3371525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$32704EDA-9185-41BF-A675-36662AA3A0F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eaaee3a935b71da0c5fd895e355092a513197bd2","datavalue":{"value":{"entity-type":"item","numeric-id":3265659,"id":"Q3265659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$A5531FB9-B888-4F7A-A4DD-19E4C663F13A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75d1afab553a076377438d858db64e832299bb0a","datavalue":{"value":{"entity-type":"item","numeric-id":5916291,"id":"Q5916291"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$AEEE9E3D-147D-4BA8-BF83-4FF49AAA1482","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"272b100438791ebf9cb00211c08c13b3ce04aa14","datavalue":{"value":{"entity-type":"item","numeric-id":4428879,"id":"Q4428879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$57C21E36-C2D8-456E-9332-448E77FC20F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76c47ac64788248a40d8543304d3dd3bc25cb13b","datavalue":{"value":{"entity-type":"item","numeric-id":1603701,"id":"Q1603701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$7ABDA34F-AEAC-45AE-AC8C-564C5D0C153B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0657a4a1147eacb344e4c976a1cbee11aef13a5","datavalue":{"value":{"entity-type":"item","numeric-id":4925031,"id":"Q4925031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$9D37E233-29B1-46E4-9028-3AD0AAD8121C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0b93d9c315351fa9cf69a1355cf6b0795292900","datavalue":{"value":{"entity-type":"item","numeric-id":3647218,"id":"Q3647218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$77632728-E8EE-4498-886A-BB16BF2E1ADA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10ff9e50d48cc7f224534b84074703d5675af0a2","datavalue":{"value":{"entity-type":"item","numeric-id":4263800,"id":"Q4263800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$0A721B98-181E-418B-B93C-121E6D1D2C7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5c65c1f0644e24566ab5222413e6f73b0c327de","datavalue":{"value":{"entity-type":"item","numeric-id":3188334,"id":"Q3188334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$7197EC0D-ED09-4C25-9A38-41D3A382106D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af9616b003d703f9d09294a2db2e4505eb229f58","datavalue":{"value":{"entity-type":"item","numeric-id":5310891,"id":"Q5310891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$B851C63F-27B3-4DA4-A540-EA29C0B7B95E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a0428b01adcb80a4007c1543535f770bd56ed1b","datavalue":{"value":{"entity-type":"item","numeric-id":1733062,"id":"Q1733062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$39D6C91E-8406-4FC7-AE41-F3287AA79FDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"842b56d1e792f42e670c8d166b3e57b0abea925c","datavalue":{"value":{"entity-type":"item","numeric-id":3703869,"id":"Q3703869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$91E1C0E7-40B0-4D4F-A859-E1D6E8C6E95E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ac1ee249c73c16d45e6922836fb575790a28b14","datavalue":{"value":{"entity-type":"item","numeric-id":3353014,"id":"Q3353014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$AF0C1503-544B-4335-B7D0-6545781715A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b16e98f2ed75b6b2c580aaaf672acd628aa682d","datavalue":{"value":{"entity-type":"item","numeric-id":2914747,"id":"Q2914747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5919012$B39C6EF3-29E0-4C9B-9121-58F7F48215D9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d853f8523304e7a31ccf88b8ee238ef5f2ae166c","datavalue":{"value":"10.1007/S10817-020-09555-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5919012$2B678E77-E364-4AF9-9C55-03DBD222790B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3584056569ddda2ae157e968f9bdebbfa575fb9e","datavalue":{"value":{"entity-type":"item","numeric-id":5916291,"id":"Q5916291"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3c56fd475b727f5ddac8415cab36918f4504635","datavalue":{"value":{"amount":"+0.9990814328193665","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":"Q5919012$CABAF639-8B91-427A-99AE-1E0CB08B72B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a1a12c1e0a5a77e2f0e3ee42f30fdeb4e0ae403","datavalue":{"value":{"entity-type":"item","numeric-id":4948542,"id":"Q4948542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad6dd1d1f9ae5ea134b80e8d04c67c8ae825ef05","datavalue":{"value":{"amount":"+0.8150107860565186","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":"Q5919012$5D4C2A36-6EC9-4DCE-99C9-8E7B7D25C9FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"309a2fb3896afcd614632ddfda96b918cd9d9580","datavalue":{"value":{"entity-type":"item","numeric-id":3838821,"id":"Q3838821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad6dd1d1f9ae5ea134b80e8d04c67c8ae825ef05","datavalue":{"value":{"amount":"+0.8150107860565186","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":"Q5919012$106E40E6-7E34-4434-952E-FF227D15159A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45fa58d2ca97e0eb245fbc94019da0ce6de22ebd","datavalue":{"value":{"entity-type":"item","numeric-id":3647218,"id":"Q3647218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d01aa39d5b85f27facbf6fb8fc790a059d89d6c2","datavalue":{"value":{"amount":"+0.813386857509613","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":"Q5919012$C407831A-BAF1-4996-B391-C2A179CCCF5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"966babd98e768c93a518015a70490aab9f42ac29","datavalue":{"value":{"entity-type":"item","numeric-id":4263800,"id":"Q4263800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8ed0600c646df27809a4f7c0be31e8a65f76fa7","datavalue":{"value":{"amount":"+0.7673062086105347","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":"Q5919012$E5C8B9B0-DFCB-47F6-B3BB-D8975ABD1EDD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Constructive decision via redundancy-free proof-search","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Constructive_decision_via_redundancy-free_proof-search"}}}}}