{"entities":{"Q40509":{"pageid":40565,"ns":120,"title":"Item:Q40509","lastrevid":105428072,"modified":"2026-10-09T10:09:01Z","type":"item","id":"Q40509","labels":{"en":{"language":"en","value":"Verified Prover"}},"descriptions":{"en":{"language":"en","value":"AFP entry Verified-Prover"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"afe2dfffa19eb48e9aaae7f3afc00c2190c73d92","datavalue":{"value":"28795","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40509$0A0D8B43-1F38-47A6-AE0A-B59ECFC7695E","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":"Q40509$F9DEDA89-91D1-4472-A2BD-AA0FDEDF12D2","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"00181b351f8a0200fa25b3d89aa775357a496e88","datavalue":{"value":"https://www.isa-afp.org/entries/Verified-Prover.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40509$84BB1590-AFF3-4283-9798-B77CF326FE36","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40509$467F3018-F3B5-4156-8D12-6C55FACC3739","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40509$CEACC7DF-83F3-4BF3-8D2E-2D64CC4BE9E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40509$FC4DEC2C-B1BC-4924-B558-17B34D369B6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40509$E1D7922F-627A-4E69-9A5E-4327C630BBF1","rank":"normal"}],"P1458":[{"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":"Q40509$A2348B4F-06A1-4FAD-BF91-F5B076FDD53A","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":"Q40509$F1F32213-BC83-4177-A3A9-5D9E931351CB","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":"Q40509$DAAD8B63-84C3-4A42-8605-59113A35C147","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":"Q40509$B509C2C6-2F49-4D24-89A1-3CAE9C7CF869","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":"Q40509$15D7199A-CAF9-4664-921F-9B5581D95181","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":"Q40509$ED646136-76F0-4E94-8952-5080EF273CC0","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":"Q40509$EAC75EF9-BD6D-46CD-8760-706B520D412F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40509$4AEDE725-9F3F-4FEA-A61A-2CC4DD30AB75","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":"Q40509$4C5C152E-CB75-4D60-AE73-6EC69F093326","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40509$11511644-0236-497F-8EE7-EAD032EE0D88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"dc75b1f4f41a196c347c039c5eec89b08662123b","datavalue":{"value":{"entity-type":"item","numeric-id":18543,"id":"Q18543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40509$BAC1D6B3-C4E0-44F3-9017-FA35FF48D766","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":"Q40509$1377091E-B8DC-402A-A0DC-5711FA447919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"053ea061eb2db1c9b7f27b25da993bb19055407c","datavalue":{"value":{"entity-type":"item","numeric-id":25224,"id":"Q25224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40509$5960B83A-9F81-4A98-B77F-2D25A96601F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"18e15e946a9b8db60c88d8c0a9a054a3d76ac633","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40509$0519D783-8BAE-4C55-B41D-2BC87116A4FE","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":"Q40509$D71BC6E6-4EC2-4734-B8DA-0A3E183E7C23","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":"Q40509$793667E3-A8CE-42E0-B11B-4BD96CA859C1","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":"Q40509$E7F60EDE-48D4-4C33-B4FF-984BA5C35830","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":"Q40509$464960EF-63DB-4756-BAB8-F06BF6CC58D8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9f8d73d41a7118cd35451f50833b47ab3d5c3c46","datavalue":{"value":"https://isa-afp.org/entries/Verified-Prover.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40509$A8057353-B8D0-480A-ADD4-214ABF1C40F6","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"cdcc065143ef05b577fcf1932e0ad33c387a57fd","datavalue":{"value":"Tom Ridge","type":"string"},"datatype":"string"},"type":"statement","id":"Q40509$242DE909-E276-4F15-9BB4-35334456A810","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"340427196063b30e84f895e7a9b885ebea5035f4","datavalue":{"value":"Soundness and completeness for a system of first order logic are formally proved, building on James Margetson's formalization of work by Wainer and Wallen. The completeness proofs naturally suggest an algorithm to derive proofs. This algorithm, which can be implemented tail recursively, is formalized in Isabelle/HOL. The algorithm can be executed via the rewriting tactics of Isabelle. Alternatively, the definitions can be exported to OCaml, yielding a directly executable program.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40509$4342D6AC-4416-4057-925C-E84F972D34D2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40509$038B2654-105E-4258-925A-75649EBDA51E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b750f44387e6c68b70dbe9597c5ea0f05f5c67d","datavalue":{"value":{"entity-type":"item","numeric-id":3138826,"id":"Q3138826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40509$847224AF-55FD-4D8B-892A-D84A1FCE7653","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"850edc50bef9caa94346e9c54c5c7bf7ffb47f31","datavalue":{"value":{"time":"+2004-09-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40509$B4D8DE79-3A02-4D78-82DD-6962B911F320","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f7c4a3e3c44b53225a7d26454edc48ea2705f618","datavalue":{"value":{"text":"A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40509$72435F5D-726B-430C-9B72-6F86E9C1C5CB","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":"Q40509$C994B8FD-EF87-4B0C-B00E-340CCAA7E644","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"fd4ac40fec1edeb460421a77e059cfe2df479821","datavalue":{"value":{"entity-type":"item","numeric-id":7360812,"id":"Q7360812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40509$A25AF662-53AA-46DD-83FE-F1CA97086C40","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verified Prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verified_Prover"}}}}}