{"entities":{"Q7361517":{"pageid":31520090,"ns":120,"title":"Item:Q7361517","lastrevid":105367982,"modified":"2026-10-07T13:37:19Z","type":"item","id":"Q7361517","labels":{"en":{"language":"en","value":"Automation of Boolos' Curious Inference in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"AFP entry Boolos_Curious_Inference_Automated"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ecf8cee4216b1b318dd40ca8a758a5beffcb8d66","datavalue":{"value":"https://isa-afp.org/entries/Boolos_Curious_Inference_Automated.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361517$8CBEE624-FD73-4F2F-AC37-EC9DFAA8CFCB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f0a25f233647d1bcbaee47b52fc4ae8005a47e7d","datavalue":{"value":{"time":"+2022-12-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361517$BE7209B3-4D3D-49E2-91B6-EFB27EA78BB5","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"c02d9ad114c3bd598ff935febd6964e2e7a5f3eb","datavalue":{"value":"Christoph Benzm\u00fcller","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361517$9C61EDC7-6CB8-41EC-918C-453494436627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"479a94397b8aa1bf4533d78980d18d4e8d7f3150","datavalue":{"value":"David Fuenmayor","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361517$6440DBFF-A168-4B70-A33D-900EA7C98DFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"7da4da03144ea1c47d9fdb504fbd6e02cc7d4783","datavalue":{"value":"Alexander Steen","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361517$DAA1E4AE-7BFD-4397-983E-1CD915CE6F7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3d99b32b9c02d41e46ad8d84fb60adae5393326d","datavalue":{"value":"Geoff Sutcliffe","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361517$CCF0A454-E68B-4393-A939-CA3736A3F108","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"de28aecfbb8a926277dde1a17114e74b04e93727","datavalue":{"value":{"text":"Automation of Boolos' Curious Inference in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361517$A519F336-06B0-4350-9600-B309AD5EB6DC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"dd432eb14ad572a32f83ef42449383d0f14484b1","datavalue":{"value":"Boolos\u2019 Curious Inference is automated in Isabelle/HOL after interactive speculation of a suitable shorthand notation (one or two definitions).","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361517$E4D5347B-972C-4305-8D86-099662BC5C7F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7ae45f11d039b13e3537bd38c8b726270d8fca6","datavalue":{"value":{"entity-type":"item","numeric-id":1437034,"id":"Q1437034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$9F12B257-5F8F-4E6F-B61F-B205303EF1B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b11646dfc2677d6614fa16128dbbd7844776606d","datavalue":{"value":{"entity-type":"item","numeric-id":1847766,"id":"Q1847766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$86F9E495-8F18-41A4-A84D-64880A4F9096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f84661190c70e049933b7bb825904abf4b4a875a","datavalue":{"value":{"entity-type":"item","numeric-id":908896,"id":"Q908896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$95DFDBA6-D8D1-4003-8D33-F58E4981195B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85b58e334bbf84629d414ca7d6688164e5524fe2","datavalue":{"value":{"entity-type":"item","numeric-id":4726218,"id":"Q4726218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$0DC8E8BD-2754-4B74-B1B3-4FF913BD0AE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"565e2039f16dc5757baa41da9dea1aaabca87213","datavalue":{"value":{"entity-type":"item","numeric-id":1091390,"id":"Q1091390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$7E90A4C1-57A2-40EE-82E1-9789EEB2F12F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cd44858abd76ba6a4654ef8a7945fafeb171c3b","datavalue":{"value":{"entity-type":"item","numeric-id":1057847,"id":"Q1057847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$61E029B6-EEA3-4570-929F-1511819566D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba16d3643e7f45b2a6fcdd3509fdca985c4702c9","datavalue":{"value":{"entity-type":"item","numeric-id":2589521,"id":"Q2589521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$B6BCECE0-D993-4CF8-AB37-A381D3339724","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$BC6F09E4-79D7-4A94-80BD-47C19BFDBBEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0d2e680f9a486f4f81eca75f944e3c75c5e0785","datavalue":{"value":{"entity-type":"item","numeric-id":4707764,"id":"Q4707764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$CD234F91-D6C2-47A2-88FC-6EB846BCD9D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9297b6a91a7c29eb2b70ce4159ebd40915c17240","datavalue":{"value":{"entity-type":"item","numeric-id":2305435,"id":"Q2305435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$D9B2E5A4-1FD8-4B0F-9CD9-4E9EA3E2EA01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93b0ece7e2512715165615b2a0e8d68cae69210e","datavalue":{"value":{"entity-type":"item","numeric-id":5760848,"id":"Q5760848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$CAC3CBC6-33FB-4884-9151-7C74E16BD37B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7f4338d79de40b34fd30046415813d87c344b6","datavalue":{"value":{"entity-type":"item","numeric-id":2405245,"id":"Q2405245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$08729280-639E-4C19-BE5E-584C2CE9C8E2","rank":"normal"},{"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":"Q7361517$9CDA7C04-7883-4DD7-9BD7-6D771BF42A68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07d763717b639e10adfdb52f6d0aed821444ad5f","datavalue":{"value":{"entity-type":"item","numeric-id":2907353,"id":"Q2907353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$87BC4240-556B-47E8-A3C8-248CB6AC1949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bf8aecd07fcc32df62578a599f73a6cd95aa21c","datavalue":{"value":{"entity-type":"item","numeric-id":6639602,"id":"Q6639602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$19A704B8-7DAA-44C7-89CB-019D06F6E339","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60c17e21a2733b0ecb5958310c8a2fecb54bfb3b","datavalue":{"value":{"entity-type":"item","numeric-id":2287904,"id":"Q2287904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$778ADD95-4A2C-41C6-90F5-B1ACFC1C0804","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a44f29a5847ba65ecb038e53a168893c35ebafbc","datavalue":{"value":{"entity-type":"item","numeric-id":287283,"id":"Q287283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$B9C58801-9126-42D3-AE80-FB59BF55A51C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cafb1aab48a88bd1a080c979a206fc7fd624f321","datavalue":{"value":{"entity-type":"item","numeric-id":2666959,"id":"Q2666959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$91EF5622-C988-4B5C-B33F-56892B2D1FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5552c73af9ffa4d08773105bfa675feb6642eb2e","datavalue":{"value":{"entity-type":"item","numeric-id":3453119,"id":"Q3453119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$E8B98039-9ED2-4219-BE0E-44C36F9EC974","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81006082b42235e7fe4c4265102798be7adefd9f","datavalue":{"value":{"entity-type":"item","numeric-id":3648679,"id":"Q3648679"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$CBB3213A-77DA-4023-BA9F-6C67E21040A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95ad3748c26d7907a9b2a2e66ec00a80dbda987f","datavalue":{"value":{"entity-type":"item","numeric-id":1868166,"id":"Q1868166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$CBBAD515-526D-40E4-9AF6-F65F09B0DC18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad1bdd6abc4d3cf5dea2b7602404acd1281c9b7d","datavalue":{"value":{"entity-type":"item","numeric-id":1799072,"id":"Q1799072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$ABD6FB03-3C2A-4551-B3E4-1AFA8E16FF2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7cdc8410680f0406092d6e0bc4dd9194588d339","datavalue":{"value":{"entity-type":"item","numeric-id":1978469,"id":"Q1978469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$E6584653-74E0-47FE-BBD6-6577642E03DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ee178f7541c5d2ed1d6ee17e1e99ce6d2d8a20c","datavalue":{"value":{"entity-type":"item","numeric-id":5195271,"id":"Q5195271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$2FD1E001-C7D2-4F08-A739-82D99917E555","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"775c0fbb82731a41620bf40f868b011533300a54","datavalue":{"value":{"entity-type":"item","numeric-id":6200767,"id":"Q6200767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$01886D29-7BE0-461E-8550-B9D04ABB3465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea4ee858c8544ddaa2b36ea8b7a73636ae5df893","datavalue":{"value":{"entity-type":"item","numeric-id":3075241,"id":"Q3075241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$981F8E39-2CCB-4509-9184-C143145E1D78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f82f0f40ab66cf033c5a229880b34de6b2284f9c","datavalue":{"value":{"entity-type":"item","numeric-id":1694574,"id":"Q1694574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$0AC65FB8-71C0-41D1-95D5-18D260FCF2CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9bbc9cdd9667523730b17037c3549c772dd39af","datavalue":{"value":{"entity-type":"item","numeric-id":5918381,"id":"Q5918381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$BC378386-307C-4FA0-8634-23F2E017E976","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":"Q7361517$53CEE942-AE4B-455B-878E-3CAFDC9624EF","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"1c4b73191cd9dbf7ab9ff860df36cb98a45764cc","datavalue":{"value":{"entity-type":"item","numeric-id":7360805,"id":"Q7360805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$AFFC41D4-6C6A-487C-90CC-15C781B1954A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"a455484e47dfc7544c354207cf0aa1a6f13b12cc","datavalue":{"value":{"entity-type":"item","numeric-id":7360806,"id":"Q7360806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$7EF71829-1BED-4765-912E-A1E57FE32930","rank":"normal"},{"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":"Q7361517$E546068E-B1A7-40B5-8730-F085AC4978C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"61ce00bd57c38f4b0878e61948aa744910b408d4","datavalue":{"value":{"entity-type":"item","numeric-id":7360807,"id":"Q7360807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$A3CCCA37-A119-4032-8BD0-33962EA9B8A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ce3280e9ef2fb44c844e03b65b6366a348e2eeb2","datavalue":{"value":{"entity-type":"item","numeric-id":7360783,"id":"Q7360783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$DF7D399D-84B8-4D2E-8269-FE8980805BF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361517$4C0D9474-3105-42C8-9A83-26EF27AFEAF1","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":"Q7361517$4E3E9836-C714-4A56-AA8F-4D5CC7C244F9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automation of Boolos' Curious Inference in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automation_of_Boolos%27_Curious_Inference_in_Isabelle/HOL"}}}}}