{"entities":{"Q2303255":{"pageid":2313998,"ns":120,"title":"Item:Q2303255","lastrevid":71799045,"modified":"2026-04-14T00:37:02Z","type":"item","id":"Q2303255","labels":{"en":{"language":"en","value":"SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7176612"}},"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":"Q2303255$0D9D80D3-ECAE-4E83-9AE8-FFA70DD24D20","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"103fe8a2e62d3280fd6a9c825e5a966f895a3003","datavalue":{"value":{"text":"SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2303255$570C4473-D3B0-4BB8-8177-31A50CEF9CEA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"862ba78b0e94c14ca0509b93e5ea9c26629ab269","datavalue":{"value":"1468.68308","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303255$5B6DB7FC-4A0A-4842-A8AE-51AE68194C88","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c68e2e1694746069837183ce414b2e41c22d965a","datavalue":{"value":{"entity-type":"item","numeric-id":2180213,"id":"Q2180213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$07CCC38E-0173-45A6-A7A1-8D2938679D38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e858e644a5f8f9e799cff3da307c11b687abc60c","datavalue":{"value":{"entity-type":"item","numeric-id":831914,"id":"Q831914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$39C3A990-9580-4208-824D-448719FEBF5D","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":"Q2303255$ABB7BD8F-3D8E-4F51-9DB5-A41B69946309","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"61e2e5951dfff50ebb9b8606073c3ef7da57bd09","datavalue":{"value":{"time":"+2020-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2303255$1DAF2557-36F6-462F-BDF9-E94C48C852FD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"56be7f8b7ec10d765565e86a364e5247a2c3c655","datavalue":{"value":"https://hal.inria.fr/hal-02965030/file/main.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2303255$E2107D7F-BA04-4465-833B-86811E5490B4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303255$40A0FE14-92C4-4BD7-9FB3-4658296AA9A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303255$3BB6B25F-2B71-4BE7-8386-8FFAF8F8BA35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303255$052C20C2-4565-47C9-8FA8-27C74F617D90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303255$2A35C3C5-8BA9-4F42-9A4C-2242E4B01949","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"90e8b8a3538c96e48b211232d775dc30d8a5c0ef","datavalue":{"value":"7176612","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303255$310B60CF-3344-431E-BB72-B879946F2718","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a313369d6da90dd1bef2143dee22ad776773a0ec","datavalue":{"value":"first-order theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303255$BD4C44DF-7495-4FC2-BC75-1C1964D79741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"57874edeb1a8d92efa1fa31b93fbd968ea8af7d7","datavalue":{"value":"model generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303255$7C9D791F-765F-4A41-A225-887B879E16F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48fe5da30f2000a910dd1a06f280ea2b3174328d","datavalue":{"value":"decidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303255$CDDDF75B-DADF-4103-AEBB-9B379DED6AC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1bfbcf77d890928584cc324fc0fed163025a3417","datavalue":{"value":"approximation refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303255$D5048EB3-0DDE-4D62-9122-9891B0788789","rank":"normal"}],"P1463":[{"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":"Q2303255$398C771E-2F6B-4764-9DA0-7AD812A01028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"83e2dec25ea583652d0e07d4393a843812f4b48b","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$2CDF424C-622B-4032-8DAD-D63F290963CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90c7c18880caa813a6bdace0f373d3dec3147690","datavalue":{"value":{"entity-type":"item","numeric-id":40350,"id":"Q40350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$F25FDF31-59ED-46F6-BE1E-00F34D012B2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$2AB21B34-1C02-4168-AD04-6588F2DF04EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$CC5DD764-92FD-4953-B31D-FF7C6C3273F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"35d91cdb711a170a910b87f452fe7b719797aa1c","datavalue":{"value":{"entity-type":"item","numeric-id":23845,"id":"Q23845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$9D82C8A2-687B-4B72-9B89-903ECE8E0D1F","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":"Q2303255$2AA19531-6ACB-42B4-AAFE-5CCA7A31FB85","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e5dce39a4673c0ce88b793cf870bff4b83262c80","datavalue":{"value":"W3006784105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303255$57980E2F-0F97-436F-949E-13F46A45A140","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$7FD358AD-1012-414F-A2A1-01A2A82BC17E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d2cf835bd77f96d03dced45b87a25996d25db85","datavalue":{"value":{"entity-type":"item","numeric-id":3158528,"id":"Q3158528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$B52C757D-4292-486A-A14B-A4CB0D58BEAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a61f4d746cc240c7e01e374e1c8b6bcf1fdd307f","datavalue":{"value":{"entity-type":"item","numeric-id":1262749,"id":"Q1262749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$929759FF-DE56-44C0-90C2-6DFC50814ED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b07bee7e03caec103786e5014f6d4794b8bbdd6","datavalue":{"value":{"entity-type":"item","numeric-id":5900727,"id":"Q5900727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$02B1320F-85BD-41D8-AFF8-58A11FE76E57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f0b555d657cb1f5a17dad4f6c65786062114626","datavalue":{"value":{"entity-type":"item","numeric-id":2487870,"id":"Q2487870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$DC5639E5-380C-4611-8DDA-307FC59A51D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"250152f4757232a993d72bf46f4fcc6e4ea0ffdd","datavalue":{"value":{"entity-type":"item","numeric-id":1041797,"id":"Q1041797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$CBC55AA1-F290-416D-88D8-36548637D029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"550580d557f088286aba342154f1791d455173c2","datavalue":{"value":{"entity-type":"item","numeric-id":3838762,"id":"Q3838762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$F7C02529-B2E8-4EF0-8010-F030A1D9060C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33890b7faad584193275d91a4cd4d3b147aff5a7","datavalue":{"value":{"entity-type":"item","numeric-id":3541709,"id":"Q3541709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$299BE42B-C0BF-43AF-9C5F-D55C5C943A19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abd7c21ad90e0dd8485a1544cb35dfb6ee469ffb","datavalue":{"value":{"entity-type":"item","numeric-id":4916080,"id":"Q4916080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$9D2F2EEB-2413-47D5-A51F-4C2355C5A3DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24aa5748fbc8c25393b98a6f9e124b8c7a2afda5","datavalue":{"value":{"entity-type":"item","numeric-id":1944188,"id":"Q1944188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$4DB7079E-C226-42BB-96EF-5133B8A31BAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86c30dbffd9cb9bfe496dba980d3d8a38abe5f7c","datavalue":{"value":{"entity-type":"item","numeric-id":2892769,"id":"Q2892769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$4EF91E24-7F55-4240-A732-74A598097FD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db2ca836704dcf65f83436ff80963ebea239f750","datavalue":{"value":{"entity-type":"item","numeric-id":3593070,"id":"Q3593070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$B5C0234E-87CF-4346-B52B-FCD7235B911B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1da36e29873f6436a847324e09e33ec26ef360e7","datavalue":{"value":{"entity-type":"item","numeric-id":4385441,"id":"Q4385441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$8F35EFE7-E455-43B4-9F50-683859BA8F8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72857eab035e148de2ad6ba24027d5984b9b7b85","datavalue":{"value":{"entity-type":"item","numeric-id":5747783,"id":"Q5747783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$46C3F635-EBCC-4B40-8688-5EB5793DA998","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$16A5418D-7FF6-4CC0-8259-B6D94AB0BB74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd2ff20d65c415e5d6cc06df5bb727ff6d33d858","datavalue":{"value":{"entity-type":"item","numeric-id":2180214,"id":"Q2180214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$FC525F62-6C93-46B7-8F09-21BA385C1764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7aaed4080844d98e27bd740dafe4d38686a8e02","datavalue":{"value":{"entity-type":"item","numeric-id":2964455,"id":"Q2964455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$7E614C0C-1136-4517-8324-D7B1A1B74C69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa8bde0015d088624f82c6009f40826754b7db1e","datavalue":{"value":{"entity-type":"item","numeric-id":2405251,"id":"Q2405251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$2305046B-5CB5-4D48-9CCE-8115D42B800E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa6750f3149d248c4e232f6fdbdc36d7bc86e39","datavalue":{"value":{"entity-type":"item","numeric-id":2920991,"id":"Q2920991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$E54D05EA-E1FA-425A-97B2-7770AF75A78E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43f8b81729c278d2b25a84d10accbf70874b133d","datavalue":{"value":{"entity-type":"item","numeric-id":4263167,"id":"Q4263167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$292527E0-6EA2-4F69-BF61-C1E9EB90F49B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00230673e703c339b2d770b71ef179a8241cadd5","datavalue":{"value":{"entity-type":"item","numeric-id":2270573,"id":"Q2270573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303255$544E5A19-D63A-411A-861F-AA40151D2523","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"81563794b9b0af5f26b20d51bea68ba653c9d510","datavalue":{"value":"10.1007/S10817-020-09546-Z","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303255$9606BF2F-DAD9-4E4D-BF29-8C4667831844","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e5172a92f343de86c9809e312fd2211d411a7d7","datavalue":{"value":{"entity-type":"item","numeric-id":2964455,"id":"Q2964455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1b4e9f57cb5f6d5ff309a037aaa3731f91e34d7","datavalue":{"value":{"amount":"+0.8081073760986328","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":"Q2303255$CCB0E68E-6862-42BA-BE50-2691EADA676D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37e2196d1c25b26a0816494b15efbc1a5da47984","datavalue":{"value":{"entity-type":"item","numeric-id":4647508,"id":"Q4647508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9f24bd061f7b119b579f9762938ed521e303a71","datavalue":{"value":{"amount":"+0.7361660599708557","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":"Q2303255$FF86FC24-0C38-4E12-9D46-C4EE73B648E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48a3d434253ed919faa661b14e883ac27b635cfa","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd33198e37188cbf064d1ec3ce317c5b3eaaad21","datavalue":{"value":{"amount":"+0.7285593152046204","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":"Q2303255$2D2EC90B-5C7E-49C4-9438-646812BA851D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f85415bc5243ca4fb021999aff0a144e42ebf84","datavalue":{"value":{"entity-type":"item","numeric-id":3541709,"id":"Q3541709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"743faab827658a9d4a0b76a7d1a542320dab46b7","datavalue":{"value":{"amount":"+0.7238715291023254","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":"Q2303255$85B33393-61E3-469C-9A57-A1A28DF459AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1f91f2a04af7ed716280a69b31bd5722b64e604","datavalue":{"value":{"entity-type":"item","numeric-id":4246725,"id":"Q4246725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b25668e714c7afc3237684bb08ec5d171489ef71","datavalue":{"value":{"amount":"+0.7184813022613525","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":"Q2303255$8D008A41-A2F4-468B-A902-9934323BAB36","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/SPASS-AR:_a_first-order_theorem_prover_based_on_approximation-refinement_into_the_monadic_shallow_linear_fragment"}}}}}