{"entities":{"Q2829278":{"pageid":2840016,"ns":120,"title":"Item:Q2829278","lastrevid":83751854,"modified":"2026-05-07T10:50:01Z","type":"item","id":"Q2829278","labels":{"en":{"language":"en","value":"AUTO2, a saturation-based heuristic prover for higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6644759"}},"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":"Q2829278$2A00A16B-0695-408D-8A56-5446CE5B5607","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8b4773c3a400d3de5a42c2275498a897a129db25","datavalue":{"value":{"text":"AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2829278$AF9725A0-CFCB-49E9-A1A0-A7AE6B67DBAD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ba43ff233e44b4e310613270e464eb230db7b356","datavalue":{"value":"1478.68439","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829278$3E56CB94-1FB4-4580-AC38-BEC07BB3C4A0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1ed1683b72bb563eae03a29cbcf732d7af63917b","datavalue":{"value":"10.1007/978-3-319-43144-4_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829278$116967C5-C673-4C42-8E5D-4FCE6AA32F5A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d47a0b532fadc119a2da0b4f59e3906ea7d12d94","datavalue":{"value":{"entity-type":"item","numeric-id":258840,"id":"Q258840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$909806F3-0AEB-434C-9385-711DF79A2E6F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$4E53B299-EB97-4902-A443-B8BECE05DEF9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3adf6ceedb6d880e3aaf819e51e828456bb3558d","datavalue":{"value":{"time":"+2016-10-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2829278$FE7C7A9D-3B27-41D8-BC45-FBA3CDCA926C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ca81a843ad968c50d84c42854e9469ce743cc3cc","datavalue":{"value":"https://arxiv.org/abs/1605.07577","type":"string"},"datatype":"url"},"type":"statement","id":"Q2829278$DC3A9656-DBC0-4DFC-910E-856AAEAD7E59","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829278$82B44796-BA2E-4480-ADEE-A41F2C80890F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f6d4b3012578fba2d8ab6b9e39d328cad9def57","datavalue":{"value":"03B16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829278$CECA42EE-1E91-40D4-9651-8B724805DEF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829278$91B79CA9-B038-43D0-AE1B-1A3FA8A68737","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"91d300e0ca9a1405c6ae7265979ca907ffefc63d","datavalue":{"value":"6644759","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829278$FE87879C-48CF-4CA5-97A9-40AAB4786FBA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$8697B535-5EF0-4ACC-850D-1040A7C6C99A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$5114C8E9-5A18-4316-ABB5-3AE4A4610C6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$FCC57B49-F734-4D89-B3EE-C51AEA846256","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$9949A6B4-3BBD-48F3-B3EE-A2B1DD80BF48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$0D321DE5-4FA6-48B8-AE81-53F244425947","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$B1AE3663-E678-40DC-A0C9-D9F1DAE013E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$6E78AA18-274D-467A-95F8-0C511B7D5053","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$429DC5C7-EB86-413A-8E91-CC1A30275876","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":"Q2829278$40685EEA-AE37-4C40-A7FA-A2AABBEDA39C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f91b28dec96b8a1bd3c88c90c8cf44cb0658d033","datavalue":{"value":"W3105824395","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829278$50B85B35-C40C-49C9-B107-AA14243AE70F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3a733cf90575ade89fba8d6309ebe3349a84d05","datavalue":{"value":{"entity-type":"item","numeric-id":2879243,"id":"Q2879243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$41952375-77D8-4509-B16F-E332CD6119A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c39b9040e3d2807bc13175b6074f0175a0a4a1c","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$4DEF9BEA-260F-4EEF-895B-0A6A25947EC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$46CC6A1E-B68E-425C-B4B1-342E22F0F8B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a1ce762817aa67ba84d34579fd3b9060a2c653","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$E2549CFF-8B34-45C3-8F45-20A9FA2AF76B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa9aacc2c379e52cdf5a99fdab1f6137b9dbbfb1","datavalue":{"value":{"entity-type":"item","numeric-id":2362206,"id":"Q2362206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$79EF2200-05E1-4BBB-B1CB-15C307E64513","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$E3CE37F7-37BF-480D-84FE-60EA0BDF785D","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":"Q2829278$6BC4613C-71CE-4116-A4E2-AFC57474B500","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0f03bf183c7a653e5e84320e58ed58d37b137b2","datavalue":{"value":{"entity-type":"item","numeric-id":1868515,"id":"Q1868515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829278$63210944-BDC7-406E-B588-62C08E5394BC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af319d95894bd51d563498fa66b2bb6f616e464b","datavalue":{"value":{"entity-type":"item","numeric-id":5191100,"id":"Q5191100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b512aa25e71ce4ac33a38921e50ecd22a4017d9e","datavalue":{"value":{"amount":"+0.7765746712684631","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":"Q2829278$F0175A25-F6D8-4F9E-9563-1E33ED3A3613","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38394b4e8d3a3502630a463829cd1f4840ac5524","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dcf6d6e9e7f62be626302d87c3532852b8149f29","datavalue":{"value":{"amount":"+0.7721508145332336","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":"Q2829278$FE991B36-4410-436D-B602-0D3E5F15A5D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d66a676533dcd495b9a796a7f6bbde83344fee32","datavalue":{"value":{"entity-type":"item","numeric-id":2908482,"id":"Q2908482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12e2bdc6ed38dd9d11c2a2fd7da3f2e31fc6d5c2","datavalue":{"value":{"amount":"+0.7633599042892456","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":"Q2829278$3E71BBE2-9195-4BA9-9956-7D5A3C418343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2a77260c5c813d21764d59a1fec5766803eafe5","datavalue":{"value":{"entity-type":"item","numeric-id":287283,"id":"Q287283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed615f97d3110c5965ca9ad4e9c93be5cd3f29da","datavalue":{"value":{"amount":"+0.7559289932250977","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":"Q2829278$962A89A1-9481-4DC8-93B8-43500D09EB82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1e2f265ef0cb2d6386b1ca06a2b615173932cf3","datavalue":{"value":{"entity-type":"item","numeric-id":5919011,"id":"Q5919011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e7c816caee463bfb57b6628b21feb7962c7c508","datavalue":{"value":{"amount":"+0.7558882236480713","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":"Q2829278$28D2E203-D596-4829-A76A-2A466F11C1DE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"AUTO2, a saturation-based heuristic prover for higher-order logic","badges":[]}}}}}