{"entities":{"Q7361541":{"pageid":31520162,"ns":120,"title":"Item:Q7361541","lastrevid":105368159,"modified":"2026-10-07T13:37:21Z","type":"item","id":"Q7361541","labels":{"en":{"language":"en","value":"Abstract Soundness"}},"descriptions":{"en":{"language":"en","value":"AFP entry Abstract_Soundness"}},"aliases":{},"claims":{"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":"Q7361541$DBE3FE4C-CC9E-4216-9123-0E700613ACD3","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":"Q7361541$3BFBD9BB-1F80-4FC5-A493-2213B05144D1","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361541$79822CBE-A522-45DB-B96F-E7BE14CB8F89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f94288ed91377510811411084214ae1d548d5352","datavalue":{"value":"Andrei Popescu","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361541$18FEA61E-683D-4797-92C0-4C08DBFE888B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2500aa80beaafa12dfa4ab6c7d8363674f762e6e","datavalue":{"value":"Dmitriy Traytel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361541$39C4A7B7-BE59-4B84-BA84-9AA4EE6D8A3E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0c1b372f5d19a59bb95ff8ae943f90c9d1d0354a","datavalue":{"value":{"text":"Abstract Soundness","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361541$9AD7FCE7-28AD-4DC4-B698-27699E56D23F","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":"Q7361541$C093CE9A-F847-44BC-8AFB-6FD0093F03EA","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":"Q7361541$18BD8A66-4E97-4C06-B6F5-E7BD3ABAEB87","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":"Q7361541$3EC26B9E-D79D-4914-90CC-D00DE4967F2E","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":"Q7361541$78AB142D-3A9A-432C-95B8-3D9C04FD08CC","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":"Q7361541$46C9768F-5C5A-4D7B-BEA1-8922FFF14166","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":"Q7361541$3BE83714-6B22-400C-82B0-EC4F50634D97","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Abstract Soundness (AFP entry Abstract Soundness)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Abstract_Soundness_(AFP_entry_Abstract_Soundness)"}}}}}