{"entities":{"Q40553":{"pageid":40609,"ns":120,"title":"Item:Q40553","lastrevid":105427286,"modified":"2026-10-09T10:07:16Z","type":"item","id":"Q40553","labels":{"en":{"language":"en","value":"Abstract Soundness"}},"descriptions":{"en":{"language":"en","value":"AFP entry Abstract_Soundness"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"5787aa6e1cfc98f8b51f020ebaa1705f28029586","datavalue":{"value":"28839","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40553$D1A3F9BF-F88F-445F-9EB7-C3E7862AB82C","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$4F0E2734-E51B-4CC5-9D3B-A96C71BFE720","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"115d8043aa98a0f0f67b3655c1ee07d81c73dcd2","datavalue":{"value":"https://www.isa-afp.org/entries/Abstract_Soundness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40553$CF158F84-5A4A-45CB-8FFD-F933920E6E06","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40553$A74F384C-A2C3-44A9-A55D-D64DBF488AA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40553$973FCC08-1752-4D9A-B0E9-02204431466F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40553$4DD3CA21-F1EE-41FB-8014-4752337A9859","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40553$A2132327-8C9D-41FE-A29E-BD3D6A3673BC","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2fd4f2f31989858180fba533a04e1a60c8d16377","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$C12120C8-1689-403C-8523-8F00D12752D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f1bbc3872a55b3dfa074c96d37fd46f076f92caa","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$7F6CFEEA-A642-45E8-AA1F-B815066F802F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$81565B45-7762-4218-9A5E-32ED015FAB82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"493c5144a9d14f0b980d45769fb4b197b51b453c","datavalue":{"value":{"entity-type":"item","numeric-id":40555,"id":"Q40555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$D90C851D-B4F5-449D-9226-A2B34E40C9D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"37701d360bad336addd4a826712aca6608c48c21","datavalue":{"value":{"entity-type":"item","numeric-id":40554,"id":"Q40554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$704D7225-502E-4830-B6BC-76300A8B79D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8bf2731143fd82a1f95f40f13b2fce56fbb7345a","datavalue":{"value":{"entity-type":"item","numeric-id":40299,"id":"Q40299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$4B6918ED-C6A1-4068-BF7E-A2FFE93886F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6953b82ed35a5241d6fb5d47b5912e5553edbeaf","datavalue":{"value":{"entity-type":"item","numeric-id":40298,"id":"Q40298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$DCE0C592-FDBD-43B7-9750-276B1272D0A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"861e34f6b532f04d877297070a58fb137923d509","datavalue":{"value":{"entity-type":"item","numeric-id":40509,"id":"Q40509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$8C3806D9-3B03-4327-806D-6E8164C747EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"5a186263bc9fb77c5d68f5852fbf845cc855223a","datavalue":{"value":{"entity-type":"item","numeric-id":40326,"id":"Q40326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$BB8A15C5-C2FB-446B-9E3C-2121273E1685","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a0a329d132b963c571723538ca5cd1b467b324fe","datavalue":{"value":{"entity-type":"item","numeric-id":40325,"id":"Q40325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$FE000A1C-7CBE-4514-9F3A-6D45451B50E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0204f081facf570c6ab1a272475183b48ae5e4f2","datavalue":{"value":{"entity-type":"item","numeric-id":40286,"id":"Q40286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$96A2FBDE-3F13-4887-B278-FE03BE578A60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7ef1082544496cdbd626aabd0ffce07a1cf4d46a","datavalue":{"value":{"entity-type":"item","numeric-id":40285,"id":"Q40285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$F78341C0-8895-4AF2-A97F-6BFB844DED80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ab75a27745b95bbc51eed60e2ef7157b7c449125","datavalue":{"value":{"entity-type":"item","numeric-id":33768,"id":"Q33768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$FF13965C-F37E-44D2-8194-14544F970D90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$E8F9233C-00B2-4761-A801-7E4383771E13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9a2aad95369d69c08086a6600b609b3220c2705e","datavalue":{"value":{"entity-type":"item","numeric-id":40276,"id":"Q40276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$C1335059-DA77-4D1A-BDB5-8DD49C70608A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a3d1e0e198e45cd480c75f3cdc16c51aa12a9827","datavalue":{"value":{"entity-type":"item","numeric-id":43931,"id":"Q43931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$1E148F38-16DE-40CA-B8C1-E3E84568E61A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"90ccaf8bd8cd77886514793cbc9a0a922682a7f1","datavalue":{"value":{"entity-type":"item","numeric-id":31430,"id":"Q31430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$214A3CED-44DC-429B-98D5-9B7E52997789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1da83e82f563b21e91a419cb34e11d3be154209f","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$1D4F3BFA-DF9D-46B7-94D4-8DB69FB7DEF6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c2c27b7f76a6830e730ddb0214f254ab15ecdf9c","datavalue":{"value":"https://isa-afp.org/entries/Abstract_Soundness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40553$0E15E78A-CB2C-4E95-8055-AFDF61C93E01","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q40553$C7121F01-7D3F-4637-83BC-8A34A5CED7B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f94288ed91377510811411084214ae1d548d5352","datavalue":{"value":"Andrei Popescu","type":"string"},"datatype":"string"},"type":"statement","id":"Q40553$EA9C47D4-3D2F-40AF-99D9-EA8A8FE8CA2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2500aa80beaafa12dfa4ab6c7d8363674f762e6e","datavalue":{"value":"Dmitriy Traytel","type":"string"},"datatype":"string"},"type":"statement","id":"Q40553$A29ABF3C-5872-45B6-BE07-E1CAEE47CC6B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"07a34b0cd8dbda78bc74e6035d9241206d157520","datavalue":{"value":"A formalized coinductive account of the abstract development of Brotherston, Gorogiannis, and Petersen [APLAS 2012], in a slightly more general form since we work with arbitrary infinite proofs, which may be acyclic. This work is described in detail in an article by the authors, published in 2017 in the Journal of Automated Reasoning . The abstract proof can be instantiated for various formalisms, including first-order logic with inductive predicates.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40553$1D97C435-9C58-4C30-A2D1-F43885547D47","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1ff77e7ec0010dc728a970344576af099b4bd62b","datavalue":{"value":{"time":"+2017-02-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40553$4404DCFF-10D5-4260-9C5C-646E8156414F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0c1b372f5d19a59bb95ff8ae943f90c9d1d0354a","datavalue":{"value":{"text":"Abstract Soundness","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40553$D6796371-9D85-4D9F-B7A3-751F63389B6A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ac39b9a75827004294f51289a3c3e79253c87a2","datavalue":{"value":{"entity-type":"item","numeric-id":2362498,"id":"Q2362498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$635917BC-706C-45F3-9C73-4D3750D03F96","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$10D9BDB1-54C9-436D-B74C-A916C6A2F5F0","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"8cff43cabc8efabeeb43dc3b07eb4f3a3fe89913","datavalue":{"value":{"entity-type":"item","numeric-id":7361556,"id":"Q7361556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$75407692-E490-4135-9B99-0CE8D8C28260","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"0010e22d998484f218097f7f79d7fc22bc7427c6","datavalue":{"value":{"entity-type":"item","numeric-id":7360817,"id":"Q7360817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40553$18867FAA-7473-4625-BCB9-926ADB7A7E6D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Abstract Soundness","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Abstract_Soundness"}}}}}