{"entities":{"Q40554":{"pageid":40610,"ns":120,"title":"Item:Q40554","lastrevid":105427274,"modified":"2026-10-09T10:07:15Z","type":"item","id":"Q40554","labels":{"en":{"language":"en","value":"Incredible Proof Machine"}},"descriptions":{"en":{"language":"en","value":"AFP entry Incredible_Proof_Machine"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"1d9d178d063667816facbba38aef3066ca604aad","datavalue":{"value":"28840","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40554$0425D7D6-3B60-45B1-8820-1E9C1798E4A7","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":"Q40554$E7B6B57F-38E9-4934-9EFD-CAFCB0FD1638","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"e2ccc3c1436200e985673526761edb74c00864cc","datavalue":{"value":"https://www.isa-afp.org/entries/Incredible_Proof_Machine.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40554$A7412B03-F86C-4AF0-AC11-3FBC2B2582AF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40554$93BE5113-202D-45C1-AB5C-1B2A6380226D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40554$87808FDF-AD08-4119-B9AC-468045EE1844","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40554$C1B36742-D79D-4938-B2BB-2C71686A021D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40554$D83CB8BB-93AE-4082-8B93-755B57601735","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":"Q40554$40106F49-34B5-4A53-BFC4-F06F84640BD6","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":"Q40554$5BC8BC29-F924-4789-9C83-550C3EC2C267","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":"Q40554$9675FAE9-7B35-4FFB-BAE4-C27D072E089E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"84465f5a171e6a9162115dbfd024a750532c07c6","datavalue":{"value":{"entity-type":"item","numeric-id":1334377,"id":"Q1334377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40554$A774D584-AFC5-485E-A0F2-5D0FB832B65F","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":"Q40554$27CAF1DA-F7C2-452C-933F-D55E5CFCA954","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":"Q40554$B86F9444-F2DC-4651-A932-23AAF56CE34D","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":"Q40554$00F82171-FCA6-480B-98DC-374E7C84F218","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b677ab36580483ca33e96c40f998e187dadaa8b2","datavalue":{"value":{"entity-type":"item","numeric-id":40553,"id":"Q40553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40554$9BD9F370-5117-4146-BE4A-A1033E8AAD8E","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":"Q40554$F2048473-0B45-4A19-B723-E741F4765A44","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":"Q40554$4F102D11-FE27-433E-A31A-286E5CB680B6","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":"Q40554$CFD4D218-793F-47D1-ACDF-F53B32F3B1DE","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":"Q40554$B618F158-695C-466D-ADF6-2F26681B9EC2","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":"Q40554$42204071-C236-4B55-84AE-C32DA7AC7DC4","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":"Q40554$FAAF2DF7-E0C9-42AE-BB90-EAE09CDB477C","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":"Q40554$23F6787D-D668-4F04-85D7-41E511112405","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":"Q40554$634B73A7-A6A9-4296-9B38-8F2E65E67223","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ed054960bcb78ae97b7ae6209e8b6255cdd32421","datavalue":{"value":"https://isa-afp.org/entries/Incredible_Proof_Machine.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40554$7035ECD3-816B-46E3-8C0F-908E6D829C16","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"2979132c44ec8ddf771d8270d088441363a82493","datavalue":{"value":"Joachim Breitner","type":"string"},"datatype":"string"},"type":"statement","id":"Q40554$7A1C26BD-66AE-4A82-9089-1224F77567DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"562d95e3e9c0f1a9cef02708fad73f14ad9bf3e3","datavalue":{"value":"Denis Lohner","type":"string"},"datatype":"string"},"type":"statement","id":"Q40554$7CF29B6C-C6B9-452A-BE65-A87948190320","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5de4eb45de6ea9587e43f2d528b90a2f75958892","datavalue":{"value":"The Incredible Proof Machine is an interactive visual theorem prover which represents proofs as port graphs. We model this proof representation in Isabelle, and prove that it is just as powerful as natural deduction.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40554$452F9BDE-C211-4BEB-992A-E911E77BB94F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"206c3c6e81f9d9944e5def066a21d9c872111ac3","datavalue":{"value":{"time":"+2016-05-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40554$351C544F-7729-4687-B095-221ABDFFB535","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7c4427bb24832baa6ecd24150b5f216edacc9620","datavalue":{"value":{"text":"The meta theory of the Incredible Proof Machine","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40554$7709D95F-F7AB-4D92-8D04-AD7837F622FB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2da17dad5fd4641d64373f0fc66dbe3dd437187","datavalue":{"value":{"entity-type":"item","numeric-id":2829254,"id":"Q2829254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40554$611C7D5D-B55A-4786-8C6C-43B052E7C612","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":"Q40554$C0401E26-BE48-4047-AABC-38A3EE9AF6BD","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":"Q40554$376EB13C-8C62-436C-842D-7B50F669E71B","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":"Q40554$FB184A65-D573-4F60-8E9D-19E31D1834E7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Incredible Proof Machine","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Incredible_Proof_Machine"}}}}}