{"entities":{"Q5504659":{"pageid":7534219,"ns":120,"title":"Item:Q5504659","lastrevid":50547389,"modified":"2026-01-14T08:55:23Z","type":"item","id":"Q5504659","labels":{"en":{"language":"en","value":"\u03b1 lean TA P: A Declarative Theorem Prover for First-Order Classical Logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5496696"}},"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":"Q5504659$E1460100-1835-4EC1-BDED-F54577038ED5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"69e758519f1987273d15cf202823da180dc2e927","datavalue":{"value":{"text":"\u03b1 lean TA P: A Declarative Theorem Prover for First-Order Classical Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5504659$0A110572-FCB6-4E97-91D0-6BC78CB9B0E2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"04daa8647ba85fa0828829e956c55ff9b99f0e08","datavalue":{"value":"1183.68561","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5504659$8A6D9F06-5D90-4BC3-B3E1-960FB3825FDF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"52544cf9010bfea118466df7f69f6b50127da3c2","datavalue":{"value":"10.1007/978-3-540-89982-2_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5504659$4B8C1EF5-323C-40B4-AE09-F2701434734E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ff82775ee47f29deeea45505b9e74b4bf9a3a35a","datavalue":{"value":{"entity-type":"item","numeric-id":2009608,"id":"Q2009608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$7F9D4BF1-D593-4442-8DCD-E01F27464BC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3dd4da07b6f95c9851a9bbf0b8a8abccf8193c75","datavalue":{"value":{"entity-type":"item","numeric-id":634202,"id":"Q634202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$3018CF0C-FB51-4E22-81F8-53FB08CD8A7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce32ac41eacedba3c0484c0c8ef4429bc69fdaab","datavalue":{"value":{"entity-type":"item","numeric-id":1101432,"id":"Q1101432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$B9D846C9-B26E-4FB6-8F6A-944892D85C7B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2c84f47c65e4d1c693c9c2179cfb504e9fb62486","datavalue":{"value":{"entity-type":"item","numeric-id":3608641,"id":"Q3608641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$205445D7-8A43-4BFE-AC12-D432346BC168","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2844be9af34a276fa39e2e4031f3513bcfe525d4","datavalue":{"value":{"time":"+2009-01-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5504659$7BC6FF8F-723C-4D81-947C-7C75A0A1FA81","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5504659$D05D8789-2B45-4FA6-904A-DCA8AC6A6C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5504659$13310845-DDF8-4F81-AD72-A597B4E5C3AE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"23930db0df58ca1cab9a04975422e8b5210d618a","datavalue":{"value":"5496696","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5504659$80310370-CF42-4630-9BF1-2AAFDFBC6356","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"70c51cb69cf83ba52d30c7a2c9abf4fc48a6f8a5","datavalue":{"value":{"entity-type":"item","numeric-id":18707,"id":"Q18707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$6E078E0F-737B-42CA-91ED-6A13366FC5ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7d71ba57e2e1006d3b877d7aaa7a6e9ff212b9bd","datavalue":{"value":{"entity-type":"item","numeric-id":21964,"id":"Q21964"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$46E47E4A-9836-42DD-855F-BEBFFE2C5A6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$09C21C29-40A2-478C-AED8-4F4D099C4E09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$55CA1091-B35F-4224-A701-1775F2B38AF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"039ee0c9703af52130b4ec7df459cd545f3e0bcf","datavalue":{"value":{"entity-type":"item","numeric-id":31904,"id":"Q31904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$5CC9603C-1F90-4A33-B82D-A8DB538B779B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a3cd421874fcb8a2dd7e34ecd62611f94d136a75","datavalue":{"value":{"entity-type":"item","numeric-id":31905,"id":"Q31905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$E22412C7-7F73-4791-BB02-9E823D3C214C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bccd1d0bb2717360c541381c661e7bb40d86b318","datavalue":{"value":{"entity-type":"item","numeric-id":21962,"id":"Q21962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$44C7720B-F883-46C0-9A4C-B32F80E9F4DE","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":"Q5504659$C620C1E6-DFA5-4AD8-B98A-A8BB5CED552B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"438157d7384cb8966c6efe632ca26fcb9b0c756b","datavalue":{"value":"https://doi.org/10.1007/978-3-540-89982-2_26","type":"string"},"datatype":"url"},"type":"statement","id":"Q5504659$93FBF560-85F1-4FB1-86F3-4772F3F5791B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"778b5788a44a396618d31d90382021b3946f001b","datavalue":{"value":"W1484198662","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5504659$3BFF76F5-69C1-4CE4-87A1-B95BE89B175C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"43f9608b13e21870d0ea96a60dac80597e508d93","datavalue":{"value":{"entity-type":"item","numeric-id":1904400,"id":"Q1904400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$0BD90F92-E7AC-4890-B710-DCB605CF5FB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ae1ae279a482446bb78d37be8963f369d811b8e","datavalue":{"value":{"entity-type":"item","numeric-id":5714442,"id":"Q5714442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$900C86A6-A773-4A82-8B35-377719E1F9AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ade402c8643377c95736cc4de881776c386a1875","datavalue":{"value":{"entity-type":"item","numeric-id":1882909,"id":"Q1882909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$1C2FA270-937D-4D68-9570-74752EC7310B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a351897245977aa0d098a2219b09f6d20cfa230","datavalue":{"value":{"entity-type":"item","numeric-id":2751360,"id":"Q2751360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$117D8336-E45F-4B67-90E1-D3D5D7847823","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2146fe71b39638fd1364e80615a2a1a9ddb51fe","datavalue":{"value":{"entity-type":"item","numeric-id":5313189,"id":"Q5313189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$DAFDE349-7776-4BA3-A8D9-CFD31A29650E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ad2e3e71fd34316c4d5dca241131f17edc1acca","datavalue":{"value":{"entity-type":"item","numeric-id":4863622,"id":"Q4863622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$195C39F0-03CF-4301-B02B-009EB557666C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42ba0d7a787c3ddf27f1ee78a59c4dec37184a75","datavalue":{"value":{"entity-type":"item","numeric-id":4520767,"id":"Q4520767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$870EF829-1F50-47A6-A5DD-FA0DC942162F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5587664e371fa7cdb52e3b1329f22cf9fcff022","datavalue":{"value":{"entity-type":"item","numeric-id":1101242,"id":"Q1101242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$C1907F3F-38E9-4C2D-A534-F467E8F45305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a645994ce7cfa21164a099b14bb38551cdb1568","datavalue":{"value":{"entity-type":"item","numeric-id":2936782,"id":"Q2936782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$F6D1CEFD-027A-44A4-83A6-5E1027D11325","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c5b09e879fc9e6d166a18cb26ec583e2bf401aa","datavalue":{"value":{"entity-type":"item","numeric-id":1272614,"id":"Q1272614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$733A41AD-52F8-42BD-AC83-659BB66C5B52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c16bedf88d37c78219926e82b3d7a7a9dee66a31","datavalue":{"value":{"entity-type":"item","numeric-id":3821629,"id":"Q3821629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$167FDD67-1C84-4D3C-814D-CE52F4A9D66E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ab938ba3d2bb1de7d34dc0f9166735f59a48b21","datavalue":{"value":{"entity-type":"item","numeric-id":1114446,"id":"Q1114446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$9FE7B657-B6EF-4AD7-88F8-5BE65A4B5CA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eba66ec3e1c80afc545116f46c6c012bf1e3a5c5","datavalue":{"value":{"entity-type":"item","numeric-id":4245942,"id":"Q4245942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$DBF22DBC-9C44-4D1C-AA42-50C097DDBEDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9a872690aae65aa8cbfced9522c07629e0a8e21","datavalue":{"value":{"entity-type":"item","numeric-id":3862380,"id":"Q3862380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$3CCFC027-7532-486C-9B15-BB48E884F067","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5e2b13fd5a27d330f592699f5bb5ff339813ded","datavalue":{"value":{"entity-type":"item","numeric-id":3789101,"id":"Q3789101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5504659$0CF923D1-DDC0-40A5-9667-AC4A8C96E352","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5fc5e20ca080feb7bd3755314bb2d0db94d1bc2","datavalue":{"value":{"entity-type":"item","numeric-id":4610335,"id":"Q4610335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31295869b1340545392f4bed2e4f0a4ced831a1c","datavalue":{"value":{"amount":"+0.7851795554161072","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":"Q5504659$4DE91852-33A0-474A-8A4B-B11F8F1B48EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8432ffbf0f85023f8e43617023893ebfe16c5bb","datavalue":{"value":{"entity-type":"item","numeric-id":4399512,"id":"Q4399512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d52ff6eab387411021953fe465c6285bd3ecbddb","datavalue":{"value":{"amount":"+0.7744165658950806","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":"Q5504659$E30B7FBC-E42B-40F7-8202-C94F4BF8E21D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c601f4f623fbf5cc4d0350b613400bfc77126ce","datavalue":{"value":{"entity-type":"item","numeric-id":3541708,"id":"Q3541708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0704609ef299718fcb96783f7644fd1a6827d3aa","datavalue":{"value":{"amount":"+0.7361924648284912","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":"Q5504659$8D3DFA43-88B8-4AED-A570-B62647DB6882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77363608aba1bdf19f0ba434a1dd2532164d45cf","datavalue":{"value":{"entity-type":"item","numeric-id":5187875,"id":"Q5187875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3bd65f3a9dfa159fc37e13ad39c81ceec2c9753","datavalue":{"value":{"amount":"+0.7160462737083435","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":"Q5504659$E69852CD-8A37-4D4A-805D-C21BD8E1473B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f849e8c0079e919fbd590217e8c1c62f3f277e67","datavalue":{"value":{"entity-type":"item","numeric-id":1404981,"id":"Q1404981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"511643bbbeba7852e8bae764ba0b0b3aa92e582b","datavalue":{"value":{"amount":"+0.7051655054092407","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":"Q5504659$09DBAA34-A8F8-4506-A750-E08EB6AF76D1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5504659","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5504659"}}}}}