{"entities":{"Q40299":{"pageid":40355,"ns":120,"title":"Item:Q40299","lastrevid":105426935,"modified":"2026-10-09T10:06:28Z","type":"item","id":"Q40299","labels":{"en":{"language":"en","value":"Abstract Completeness"}},"descriptions":{"en":{"language":"en","value":"AFP entry Abstract_Completeness"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"188598793d8bd17def2a5454c96f5c8b961b21eb","datavalue":{"value":"28585","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40299$AEBB80CD-86E6-4167-BADC-DADD70081507","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":"Q40299$F090D174-8713-4E41-812A-D1936F507681","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"388fab124e794e1256b21a547c3313f2d88e6d1a","datavalue":{"value":"https://www.isa-afp.org/entries/Abstract_Completeness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40299$7A8BC528-20BD-41DF-A0C9-C791B4CA1B64","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40299$BD2D2A21-9EBD-40A3-8DE3-0E904A25D81C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40299$B7C779AB-2B55-4A1D-8A0D-E71ED964EE55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40299$7C71878D-6E83-4F19-8685-68DABA02477A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40299$83F47B4A-F540-4C18-B3C3-D6873BDF9903","rank":"normal"}],"P1458":[{"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":"Q40299$AD30A9F5-6E6B-4185-9272-59824D181F96","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":"Q40299$F2152406-8565-4602-9D71-164CBA9A946F","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":"Q40299$7BFA60C1-3C6C-48B7-8693-953CA1C18EC4","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":"Q40299$5BE1DD52-0FBF-430D-ADAC-5933AEB980A0","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":"Q40299$3DFE201A-6836-4A55-9B48-9DCA5334A789","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":"Q40299$81EB3457-053B-433C-9798-621CB5DF51F1","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":"Q40299$206ACCD5-EC1B-47A3-8773-33AF8A157E37","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":"Q40299$B0CED53D-7EEB-439D-A575-A10F26039ECD","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":"Q40299$901C6F06-63A3-441C-BF46-C2B6D146A03C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40299$585A4B35-075C-4A6A-97B3-C5EF093BC54F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40299$C1BA21A6-C3C8-42FE-B815-3ABF991013EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40299$6F082BBB-84AA-4DF9-B1DC-5CEBE29EC009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40299$56EE1775-A0BA-4CDA-8A67-B913A4B86E99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e58bd8100179970e6dd14964997f435e21491d5c","datavalue":{"value":{"entity-type":"item","numeric-id":18928,"id":"Q18928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40299$754D33BA-2346-499F-8AF7-CFE3EB244FDF","rank":"normal"},{"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":"Q40299$81A2908B-244B-4410-8047-179E52244F66","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"153f1cf34b5de59c4798450f1cdc4714fe9b6d87","datavalue":{"value":"https://isa-afp.org/entries/Abstract_Completeness.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40299$CC425A3A-C316-4E61-9ACA-F699AC2997F8","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q40299$3C100967-A53D-4BBA-B820-DF1D284B0FE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f94288ed91377510811411084214ae1d548d5352","datavalue":{"value":"Andrei Popescu","type":"string"},"datatype":"string"},"type":"statement","id":"Q40299$FC5B25B5-3C25-491F-B8F7-9080D0719803","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2500aa80beaafa12dfa4ab6c7d8363674f762e6e","datavalue":{"value":"Dmitriy Traytel","type":"string"},"datatype":"string"},"type":"statement","id":"Q40299$36FCA450-B1B4-4AFA-8D29-E505B1A55DFC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b48ca4ad04b643a7cea889b07a14fa60276f480a","datavalue":{"value":"A formalization of an abstract property of possibly infinite derivation trees (modeled by a codatatype), representing the core of a proof (in Beth/Hintikka style) of the first-order logic completeness theorem, independent of the concrete syntax or inference rules. This work is described in detail in the IJCAR 2014 publication by the authors. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of FOL---e.g., with or without predicates, equality, or sorts. Here, we give only a toy example instantiation with classical propositional logic. A more serious instance---many-sorted FOL with equality---is described elsewhere [Blanchette and Popescu, FroCoS 2013].","type":"string"},"datatype":"string"},"type":"statement","id":"Q40299$147BC6D1-49F6-4460-996B-12D59A32BCCD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0202cb9cafa0358b07911808cfce41ae5240485b","datavalue":{"value":{"entity-type":"item","numeric-id":3192180,"id":"Q3192180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40299$DFA0B38E-62E7-4CCA-94C7-FF419C041C03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"399034269be6bba8be1aee8f83a7563dc96523db","datavalue":{"value":{"entity-type":"item","numeric-id":2849493,"id":"Q2849493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40299$D31D8443-7E6A-41F4-87CA-AF2277ED52D6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a3c251b63516e63161db6918c2e83c80c7676385","datavalue":{"value":{"time":"+2014-04-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40299$9098471A-CD3E-424C-86CC-E77F5D53E176","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"248218628c77150435f2f362489dbb5cc493e8ac","datavalue":{"value":{"text":"Abstract Completeness","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40299$BD1BDB49-82D9-4D99-ADAD-8523E51D7BDF","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":"Q40299$639907FF-94D3-4D0F-959E-160D4FCCF7B4","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"f0d6ccc9a00d2d1e3be7ec2239689671c14dec25","datavalue":{"value":{"entity-type":"item","numeric-id":7361918,"id":"Q7361918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40299$154DDE61-467A-4035-9420-04DC59F13608","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":"Q40299$87C159AF-1590-4E68-AE77-F80B5CE4C648","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Abstract Completeness","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Abstract_Completeness"}}}}}