{"entities":{"Q43931":{"pageid":43987,"ns":120,"title":"Item:Q43931","lastrevid":105428465,"modified":"2026-10-09T10:09:53Z","type":"item","id":"Q43931","labels":{"en":{"language":"en","value":"FOL_Harrison"}},"descriptions":{"en":{"language":"en","value":"AFP entry FOL_Harrison"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"9017e431ef17437ea1ec8b35cecd8dedee57e9c7","datavalue":{"value":"32220","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43931$8A2897E6-C279-4D8B-9479-3CCDDF3396C6","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":"Q43931$3D5A3239-F5D2-467A-B18B-1B6A03610E5F","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"382ef741d33e2f754c48c5afb324089bc4103b94","datavalue":{"value":"https://www.isa-afp.org/entries/FOL_Harrison.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43931$5BB29915-4114-4DB3-8422-E8936633E65B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43931$70A97880-DB8E-4B47-A64A-06719B99BA74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43931$ECF83F6B-620B-4E8A-99E8-104F1FA676CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43931$99479F08-91DA-470F-81D3-177757CBFCAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43931$9B36CA87-9709-4155-8E06-9618F1D9153B","rank":"normal"}],"P1458":[{"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":"Q43931$56FCF68A-C6F7-4BAE-BD10-B0E31ED7C5F8","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":"Q43931$BE9D6AD6-CF7B-4632-9C11-E9FF6E8B478B","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":"Q43931$86E1494F-8C22-40CC-B746-19C2191C9142","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":"Q43931$B031DC3E-A58C-4E0A-BC27-B3BD2280657A","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":"Q43931$2B284A02-4611-4D17-BCA7-7DECF2A0C9DF","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":"Q43931$66063089-A195-4DB6-9E2A-5EED4960A123","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":"Q43931$7770250E-351F-4361-B16F-BA66E4908CE7","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":"Q43931$8ECDE8BF-DAF2-4BD3-9A35-37BBA6C1084F","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":"Q43931$9E2138A0-E65B-4861-B272-DF58517D4FAF","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":"Q43931$C7808DB6-10EA-4D82-BBA8-C0010315FE08","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":"Q43931$CE768F2D-5259-471C-A103-44AC734A0D9D","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":"Q43931$ACA7D979-201C-4550-8655-8818F252073B","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":"Q43931$F729691E-E145-4075-948B-3B6FE58D9E12","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":"Q43931$3031F1A1-E821-4978-931A-C9CD472B5D4E","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":"Q43931$9588F4BF-C48E-4515-89B7-8B1E47B288F1","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":"Q43931$B454680D-1B38-44C2-AA1A-E92CE0D4A191","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":"Q43931$2063301E-A4DA-4957-AA21-05BDB6C3AFAA","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":"Q43931$BD58054E-1330-4AFD-86F9-2A57C4213050","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5c9d92dd2d96ef9a4321ff4c40281344940caba0","datavalue":{"value":"https://isa-afp.org/entries/FOL_Harrison.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43931$146110A8-6562-4D82-8725-DED5CB4432E9","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"db387998486ce4a251c290a1ea4b72600edbf89e","datavalue":{"value":"Alexander Birch Jensen","type":"string"},"datatype":"string"},"type":"statement","id":"Q43931$7B25E45B-3C46-4D30-B700-2CE7AC49BBBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f19e42813e41b1b694ee6662dce0e445e8e41f4b","datavalue":{"value":"Anders Schlichtkrull","type":"string"},"datatype":"string"},"type":"statement","id":"Q43931$F3B5BA04-E4E9-448F-868E-232DEDF96792","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"fad673ab88e4c617ff7ef906721c9d50cfb4df35","datavalue":{"value":"J\u00f8rgen Villadsen","type":"string"},"datatype":"string"},"type":"statement","id":"Q43931$428F081A-BF72-4478-B54B-670202EDA3B1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"772003d877eeed1fe375f85a4d67d8cd9b2627fc","datavalue":{"value":"We present a certified declarative first-order prover with equality based on John Harrison's Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009. ML code reflection is used such that the entire prover can be executed within Isabelle as a very simple interactive proof assistant. As examples we consider Pelletier's problems 1-46. Reference: Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL. Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull & J\u00f8rgen Villadsen. AI Communications 31:281-299 2018. https://content.iospress.com/articles/ai-communications/aic764 See also: Students' Proof Assistant (SPA). https://github.com/logic-tools/spa","type":"string"},"datatype":"string"},"type":"statement","id":"Q43931$076D3458-D599-4CAF-9BC0-3BA9DA7F9B9B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c9d2ae3d0c1afb3b001693101ae63b1db6ef1c3","datavalue":{"value":{"time":"+2017-01-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q43931$98F12795-7049-486B-A997-C5D6876AEB5E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"823b9d38036df0613ef7501d033f7846e7cb4f14","datavalue":{"value":{"text":"First-Order Logic According to Harrison","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q43931$A8B54270-9CCB-4F9D-B482-311B3A2AA167","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":"Q43931$3B6EEB3B-8F1D-4280-8ACD-26BA5C7DD359","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":"Q43931$1FEEE463-DBE1-4B00-816F-BBAAA0C2E63F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"FOL Harrison","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/FOL_Harrison"}}}}}