{"entities":{"Q4989679":{"pageid":7019256,"ns":120,"title":"Item:Q4989679","lastrevid":54006038,"modified":"2026-01-26T01:55:12Z","type":"item","id":"Q4989679","labels":{"en":{"language":"en","value":"WhaleProver: first-order intuitionistic theorem prover based on the inverse method"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7351165"}},"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":"Q4989679$FB00E805-24E2-4843-A55D-526339FA2939","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9c0a55248c58128f7ca2dfb26d761935108c28c8","datavalue":{"value":{"text":"WhaleProver: First-Order Intuitionistic Theorem Prover Based on the Inverse Method","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4989679$E0239424-EDE9-4FFC-BFF1-F1D1EFE537D2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f70a2816fd00ff7e701cba3febfb47bf9cc3c303","datavalue":{"value":"1461.68247","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989679$1FF1F2FD-FBB3-4A84-B5FF-3680FD2298A6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"59051153028c798a6cc73294e028e1c7840ddec3","datavalue":{"value":"10.1007/978-3-319-74313-4_23","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989679$868AD917-7E6A-4499-B5A0-9EDD00B1B002","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9a0dfbba4b5305381afe4f2daa1741f438642e54","datavalue":{"value":{"entity-type":"item","numeric-id":280991,"id":"Q280991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989679$4E48DCFF-6F0F-40F4-8305-1945A3EF0842","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"88e54f76d0128af9be4f85e3abdcf2e3834a39d9","datavalue":{"value":{"entity-type":"item","numeric-id":2806783,"id":"Q2806783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989679$F958114C-C7FE-4B39-9E74-7163F0DC4B56","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":"Q4989679$6F01F0DF-749E-44DB-98D0-2A4CFD12FE03","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0e6c7ff8c150409ee8b57e6f339d646c7d730856","datavalue":{"value":{"time":"+2021-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4989679$07E84EF8-5296-4E1E-95A2-7F14AF47732D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989679$61D6F9A8-126C-442A-96D8-833E5370B50F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989679$5C6FBAA0-6958-4394-A47C-393A6F678240","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"78ceb06b55a013378b7d7f7b9aaaeeb0a2f11203","datavalue":{"value":"7351165","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989679$F801CE75-092A-49E9-A1F0-7F54BE6FC254","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989679$E222A813-C467-4152-9594-D4EA43F4C064","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989679$A1010ED9-F11A-4D21-B73C-928CE1634BB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989679$B0D341C5-1754-4A05-902B-B04B6C9F1FF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f3e52067a7ed3ce53605a49bd0992ac3d371713","datavalue":{"value":"inverse method","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989679$A73ED6F0-EFC5-4F1B-9939-A80C90425CE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989679$7E5524BC-0A90-47DB-9141-5BE38234C6D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d56b66592f58cdf116cf7c3129e3ff51eddc763","datavalue":{"value":"ILTP","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989679$1E1AD034-D0D4-4BC8-980D-60F8ABF38A0B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"da80af7decb56df8eee70e5ca6b91ba167f98ccd","datavalue":{"value":{"entity-type":"item","numeric-id":45302,"id":"Q45302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989679$80A4E5B1-9EEA-4129-B090-A2B9E321E0B9","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":"Q4989679$59858624-8EAA-47B1-8A1E-67EC4A9BDE41","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"71768b9d7feecc88235a921c8cc38df61cb0dc9e","datavalue":{"value":"https://doi.org/10.1007/978-3-319-74313-4_23","type":"string"},"datatype":"url"},"type":"statement","id":"Q4989679$892B9141-F7D3-42FA-A33B-899FEA66BFE0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"28d90e12449ed3b8b8250c04b009d0aa550223b2","datavalue":{"value":"W2783704968","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989679$C23A0B99-8E21-42A8-98D6-819C402FCD70","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57dd8d582d32ac16558b5d505c52a9eeb92ab1f7","datavalue":{"value":{"entity-type":"item","numeric-id":2216868,"id":"Q2216868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"001e7782d10ff4debb8c07980cbab32539927edc","datavalue":{"value":{"amount":"+0.9332709908485411","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":"Q4989679$2CA500F4-D4CC-4877-9CDF-6F39FDA44F8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e629d1cd6ffbd991fdd8c8388457a782a8aefe2","datavalue":{"value":{"entity-type":"item","numeric-id":2806784,"id":"Q2806784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"295b83899b3866a59037cf60ed13da47fc10c42f","datavalue":{"value":{"amount":"+0.7737786769866943","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":"Q4989679$FCA830C7-654A-4F0C-8920-73390191E331","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bc88718a305d147397faaf7899d51ccdc2bb5ca","datavalue":{"value":{"entity-type":"item","numeric-id":4647496,"id":"Q4647496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"164bb56abce5ea93da407ca3142eb68d1ee342e0","datavalue":{"value":{"amount":"+0.7733428478240967","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":"Q4989679$10C8B08D-3134-4548-8535-D68CE11348DF","rank":"normal"},{"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":"2d6c314287e5f8a0d2ab5e0a6180d71c998446e3","datavalue":{"value":{"amount":"+0.7630972266197205","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":"Q4989679$60F0E14A-D7DB-40AE-B9F2-B6518E3FBCBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"569212cee5b1a71f3f06acb33bf8b257b5e9bb46","datavalue":{"value":{"entity-type":"item","numeric-id":5191105,"id":"Q5191105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b153d03d4c795ea321ece2f30dbdecf68ddd004","datavalue":{"value":{"amount":"+0.7612907886505127","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":"Q4989679$35747231-3F4E-45BD-9E84-256D114547C4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4989679","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4989679"}}}}}