{"entities":{"Q831930":{"pageid":833778,"ns":120,"title":"Item:Q831930","lastrevid":64783761,"modified":"2026-04-11T22:12:00Z","type":"item","id":"Q831930","labels":{"en":{"language":"en","value":"Improving automation for higher-order proof steps"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7497920"}},"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":"Q831930$CA54F751-7063-48F2-B87D-EF866C64D3E8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4c3bb0d1c871d83969c4c38b3b859b23b5f37c00","datavalue":{"value":{"text":"Improving automation for higher-order proof steps","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q831930$DC977CD9-EA3F-4A31-BD7B-ACE4CFE1A0C8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"df5caccf749909b712f16306a4bf4e911424d995","datavalue":{"value":"10.1007/978-3-030-86205-3_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831930$390E225F-7E9D-4E73-821B-8FF662695F46","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3d5f90b4e62a004d9940e558ff095d9e48533e92","datavalue":{"value":{"entity-type":"item","numeric-id":831929,"id":"Q831929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$AC096E58-E468-404E-ADD9-1400F4613F62","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ee216241628d7ab3ed1211164658dc9e68b98545","datavalue":{"value":{"time":"+2022-03-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q831930$B7750890-97C1-497C-9848-227FB1382A47","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"18309be7db1da1fcc09fdceba48f604c7de62db3","datavalue":{"value":"68Txx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831930$8B07ACB9-8B7E-4F97-8B1B-98BC0A91C069","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8201a120239d206764991bde70cc14b346971371","datavalue":{"value":"7497920","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831930$7730D139-0200-4F0B-871C-74FCB8BD6CF5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q831930$4E074460-756C-474C-B991-2A2130B2DA8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bffac8577b0ac0cf83610798d5a7a75e04f2753c","datavalue":{"value":"higher-order theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q831930$4CC11831-3F6C-4DEF-AB41-983F6F46E0A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"49854c860b135745c7512035241e43ede4ce7e84","datavalue":{"value":"TLA\\textsuperscript{+}","type":"string"},"datatype":"string"},"type":"statement","id":"Q831930$F8E58142-4708-4816-ACA2-C2F865808989","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"394a5ad1d2d7d06cc1b82a10ab87569bc88b3864","datavalue":{"value":"TLAPS","type":"string"},"datatype":"string"},"type":"statement","id":"Q831930$514091E0-F6A6-4D2C-BD2D-94115B92E735","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6635cd024ea0b7601d03e4b2d3631551a4364421","datavalue":{"value":{"entity-type":"item","numeric-id":21509,"id":"Q21509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$72A224A5-6975-488D-9455-006E53970A04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd2dfc4f221f8bfddd0c3de3db77eae5c6971775","datavalue":{"value":{"entity-type":"item","numeric-id":26191,"id":"Q26191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$392FF0AF-395B-4F0D-8614-B124AF231358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"491e4169c914222bc349264f15b36cbf2c3ef446","datavalue":{"value":{"entity-type":"item","numeric-id":18920,"id":"Q18920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$1E8DE48C-52A4-4115-8941-CB93A2936F6C","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":"Q831930$A77C6CAC-D0B8-4294-937D-BB074957A2F9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b43888a33bf5d631e23d44e3c0df31c265534bde","datavalue":{"value":"https://doi.org/10.1007/978-3-030-86205-3_8","type":"string"},"datatype":"url"},"type":"statement","id":"Q831930$3C3B22FF-7858-4144-B934-247471E8A389","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fd630336c190f1b98c9699af7f9330d4c58db6ec","datavalue":{"value":"W3197407391","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q831930$3D59DD63-16DF-41CD-8D23-E38187CE8752","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"126e5dfacc7f9aed01f6e192710147ed8c12ae25","datavalue":{"value":{"entity-type":"item","numeric-id":2817912,"id":"Q2817912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$F39C72E3-BB55-4EED-94A4-1D1A9AFEAB81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34d3ef919a581f437ca785956c24e2de15d403e7","datavalue":{"value":{"entity-type":"item","numeric-id":2305406,"id":"Q2305406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$41626EA3-92BC-4FF1-B1F8-3E0E2A5EF50E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d7e9017e9f92808788a0b971125d9368ce41250","datavalue":{"value":{"entity-type":"item","numeric-id":5919500,"id":"Q5919500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$F4BFF9D3-018E-4583-955B-BC623A47AAE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a7ce665db3435fa98f1acda442e827ec5d171f3","datavalue":{"value":{"entity-type":"item","numeric-id":2096452,"id":"Q2096452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$95A11C69-8C4E-4DE9-9E1D-78013A351193","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73747d1be528c82497c6517bd1ecf143bfa790b1","datavalue":{"value":{"entity-type":"item","numeric-id":2908482,"id":"Q2908482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$995A128B-EC9C-45CF-A3A3-412D465929F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ead9660cd33cf6b597620bdfac44264e0480c8c3","datavalue":{"value":{"entity-type":"item","numeric-id":4647839,"id":"Q4647839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$F7EB6A75-1BC4-4A78-ABD9-3581FF451DED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c9e64d18bb7de3b5e47887cb9581e533ff9f465","datavalue":{"value":{"entity-type":"item","numeric-id":3457789,"id":"Q3457789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$A3C5BFA9-1815-46EA-93C4-E7B09C25EEED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2542de7f09eadcdf4972d4710b463e6bf7cbbcdf","datavalue":{"value":{"entity-type":"item","numeric-id":3453107,"id":"Q3453107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$951C1D11-131E-478E-844B-18E177A0668C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d37b23b7db99d33ba41b8c893bcac4aca2de8fdd","datavalue":{"value":{"entity-type":"item","numeric-id":4870018,"id":"Q4870018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$71CC4781-CBD3-4B4F-B9FD-427BABC47515","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271e07f9c546e49eaacf117e0f5779050dbb73dc","datavalue":{"value":{"entity-type":"item","numeric-id":4934623,"id":"Q4934623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$0FE6C556-6EE6-4359-B83D-41186378EFE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad1bdd6abc4d3cf5dea2b7602404acd1281c9b7d","datavalue":{"value":{"entity-type":"item","numeric-id":1799072,"id":"Q1799072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$E6A997D7-DD91-4AC2-8CB5-D7B5D503252A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd64358c68335b8f55c95884438c93973af5783f","datavalue":{"value":{"entity-type":"item","numeric-id":5028439,"id":"Q5028439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q831930$8B4B0194-AF8B-4839-AF66-2391873D5F10","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30cc1ea5b7e5002bbf92c6fb2128ebdd9cb4d459","datavalue":{"value":{"entity-type":"item","numeric-id":4835513,"id":"Q4835513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d46c71ac3d83501d9526366ee63e27064fef673","datavalue":{"value":{"amount":"+0.89550024","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$09EEF6C1-B6D6-4A4A-875B-ED692831DC2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0ec97b8481b3a0b1d3747ab1cfe1014f767440b","datavalue":{"value":{"entity-type":"item","numeric-id":4524794,"id":"Q4524794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66a52b5f97a5daec6572450c1639d87c77a51977","datavalue":{"value":{"amount":"+0.89488924","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$8B0E2FDB-D7D3-4B71-BC6B-9B04FE4D6CBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc22a892f290f6d6ac15b5d1402ac2bb9e5071be","datavalue":{"value":{"entity-type":"item","numeric-id":2810691,"id":"Q2810691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f797dde95870e156dab84574be25514dcb5f302d","datavalue":{"value":{"amount":"+0.88321984","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$BC2CFB0E-A439-4CF4-978D-9FD510FDFAC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6706f674745437a28e826927d52883b093061b9e","datavalue":{"value":{"entity-type":"item","numeric-id":2988387,"id":"Q2988387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a5fab5180026d9bbfdad9ac2fbcbd1c12f24fdb","datavalue":{"value":{"amount":"+0.88119644","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$655ACF5B-4842-462A-ACE3-B8B6ECB4EFE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68c709b86cf7ff4047dac00daa01e8a4e28d9c32","datavalue":{"value":{"entity-type":"item","numeric-id":4023458,"id":"Q4023458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1c3adf2330a9a6e39ead42e19da73904031058c","datavalue":{"value":{"amount":"+0.87068754","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$FA461EC3-5353-4A31-AF8E-C3660A93DCBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0611c94e9ea1aaef98f6d180f8949cd0d0afe13","datavalue":{"value":{"entity-type":"item","numeric-id":3343471,"id":"Q3343471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc1ed513c2efb5b053d89bb036e54aa70ab70cf3","datavalue":{"value":{"amount":"+0.86996436","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$A1503784-E030-46E1-9142-B3CB1320CBA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bedcca7522067bd4c9657d84c45f2b6bd8d3026","datavalue":{"value":{"entity-type":"item","numeric-id":1272613,"id":"Q1272613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13b6f5acbbdb223be98852174025cebf072e02b0","datavalue":{"value":{"amount":"+0.86723965","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$6B83967B-1243-4CA8-9EE0-52F1B6E35137","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dcbb17b5eeff24acc0ae046b77968c0618c1cbba","datavalue":{"value":{"entity-type":"item","numeric-id":5204800,"id":"Q5204800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4467461f78e09075aea1f323dcdcd611688521e4","datavalue":{"value":{"amount":"+0.8660747","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$5CD7ABE5-C888-497D-B8EF-BD0603C86587","rank":"normal"},{"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":"f4626fb276156e012ba27bad0664d2bb1c4d1de5","datavalue":{"value":{"amount":"+0.860316","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$631FA387-29F0-4250-A1E2-67B806C250EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6540b6ab6d92113a91ff958757755562350221b2","datavalue":{"value":{"entity-type":"item","numeric-id":4934147,"id":"Q4934147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"726f5efabd685f0399b2a28bc36b8c611232da39","datavalue":{"value":{"amount":"+0.8575261","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q831930$E4EC2E8B-9A22-4391-BBDD-0145193C372D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Improving automation for higher-order proof steps","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Improving_automation_for_higher-order_proof_steps"}}}}}