{"entities":{"Q386032":{"pageid":387799,"ns":120,"title":"Item:Q386032","lastrevid":61448367,"modified":"2026-04-10T23:26:22Z","type":"item","id":"Q386032","labels":{"en":{"language":"en","value":"A mechanisation of some context-free language theory in HOL4"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6238119"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$82867CD1-D90B-4AFD-871F-8E5E1AC96B69","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"efc873d55ce20aa72e2f3b7f202e485de9a56852","datavalue":{"value":{"text":"A mechanisation of some context-free language theory in HOL4","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q386032$589CBB64-C603-431F-92A5-6962BDCD9C3A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0df514883f6e0f81ef382899d898b75a4493dbd1","datavalue":{"value":"1433.68531","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q386032$FD7EB982-EBBA-48CE-A827-AF79C7411847","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f503b2db75305c6c80ccf2465571a00f9a49862","datavalue":{"value":{"entity-type":"item","numeric-id":386030,"id":"Q386030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$8E323CB5-8F26-445E-83E9-D3C44D63B705","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"145fb4ab3c36a5f99f91a0be2758a779e5bceae8","datavalue":{"value":{"entity-type":"item","numeric-id":386031,"id":"Q386031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$6877B2EF-56AC-4901-A907-2E1A41D8A6B0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3340243f57e05f2265c56423c388055a14b114fa","datavalue":{"value":{"entity-type":"item","numeric-id":107189,"id":"Q107189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$C5A47413-254B-4125-8848-BAB8D74D7C96","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"53717fa6c8d29b46d6a34473fd09757844b25aa8","datavalue":{"value":{"time":"+2013-12-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q386032$3F7C0F07-2071-453E-8287-C9E5FE968A4A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q386032$50827FB0-E25F-4735-84D0-501F6E76F10F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q386032$CF906B5C-3391-4538-827B-52E96C2EA3DE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"01cc2f83d58ceebaff9caec6437fa866324fcc12","datavalue":{"value":"6238119","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q386032$6BF6AF5E-CA5F-423B-BBCA-7F36E624607F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"795414f846fccd6517b35b46d219d01dfd08d3da","datavalue":{"value":"context-free languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q386032$2AE20DBE-BAD8-4848-971D-65EB1BBAC4A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a37f1b310a3dab2e44459244c624b1e251e5b8cd","datavalue":{"value":"context-free grammars","type":"string"},"datatype":"string"},"type":"statement","id":"Q386032$7893CC63-486D-4FFD-BE61-428179A87EFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"456c672ca15cab74651e643baa7549046be81ae8","datavalue":{"value":"pushdown automata","type":"string"},"datatype":"string"},"type":"statement","id":"Q386032$4C4C5D56-7D7E-45F3-AA30-2DA9F67E52FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9a7b03c1290f4420f511d8fcb71a4d38b5c445b","datavalue":{"value":"closure properties","type":"string"},"datatype":"string"},"type":"statement","id":"Q386032$30AD4912-64E8-49B0-9ADB-E746D4166AE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8a98f4f63c134cf5f8bbe7dd8160815c1e044dd6","datavalue":{"value":"HOL4","type":"string"},"datatype":"string"},"type":"statement","id":"Q386032$994FE746-0A39-4D81-81DB-2B9B1EF5F737","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$780AD021-3104-4434-9186-62177E46F7C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$A9FF06A0-BF3E-4B8C-93AA-2A406C98A30D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"45a469a3ba8d5389be61c4f92cd274a70f310b38","datavalue":{"value":{"entity-type":"item","numeric-id":20800,"id":"Q20800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$C1AF07B2-B434-4BDA-9FE2-A22DCCC5F50D","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$6B978339-7B70-4DEB-BF41-0D7094EC5BF2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6f6eae1112dd5c3c40521d19ef5ce669cefdf18d","datavalue":{"value":"https://doi.org/10.1016/j.jcss.2013.05.003","type":"string"},"datatype":"url"},"type":"statement","id":"Q386032$AF5AB315-0B64-48EF-8CC9-A3D1FB376686","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"662ae7d1cc442ebe67ee2652f0b7b3d3e56d2d32","datavalue":{"value":"W2005008302","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q386032$20B2E67E-A509-42B2-90F4-AAF0130A7C4D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"65b596cfd231321f7e5f5e52d0f7df7bfdd20575","datavalue":{"value":{"entity-type":"item","numeric-id":3617698,"id":"Q3617698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$C5330532-CFEE-4A3D-BA32-EFD228EF2AE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f42050c132d071fca29983a6904ddd720208c02e","datavalue":{"value":{"entity-type":"item","numeric-id":3586036,"id":"Q3586036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$82E4878E-F0B5-4DD5-B861-A8B166866DE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9723e4d0f4b3ace7fe509aa62e8d21c6d7515b2","datavalue":{"value":{"entity-type":"item","numeric-id":5176948,"id":"Q5176948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$062B049B-8882-4AC8-905F-8F5D9F562134","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$69B43AAE-241E-4E05-937D-21A3633EE0FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1758902a66e2332f9d1d0268ecf38eeeb4d377f","datavalue":{"value":{"entity-type":"item","numeric-id":3862379,"id":"Q3862379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$641965D6-A79A-4597-8CE8-CFE186BE2227","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e153234bedc671890e46d97b503b862efeb995a","datavalue":{"value":{"entity-type":"item","numeric-id":3558235,"id":"Q3558235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$956EBC9B-9ACB-40EC-9F26-7FB1B1C0BC9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dbfa0add5b4a28e1b031e2492fa01fce378648b","datavalue":{"value":{"entity-type":"item","numeric-id":3100206,"id":"Q3100206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$BD91FD61-7B10-4EFF-BD88-3BD57EAA432E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q386032$004C2207-0B35-4FCF-8C5E-17DA5D218C7A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"46d89427f6d8bb7a4897c41a1516dc1f16ad277f","datavalue":{"value":"10.1016/J.JCSS.2013.05.003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q386032$CE964C4D-0C30-4461-8599-24C072D34587","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a91af2a4ed092b1374cfa3b06e47833008317d33","datavalue":{"value":{"entity-type":"item","numeric-id":2820703,"id":"Q2820703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22da4adbc35e58600bd2fd486e00f048853caf3a","datavalue":{"value":{"amount":"+0.88760024","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$80C8281B-FEA5-4CCE-A6B8-F22C98B7BE5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49c7e9456de22d5a39a9d552454c75b3d5c510e3","datavalue":{"value":{"entity-type":"item","numeric-id":3586036,"id":"Q3586036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"470f9ecfc6517a3dcf9c6968e3c4fe7ab689618b","datavalue":{"value":{"amount":"+0.88359165","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$ACDED00F-8418-4EA0-ABA0-16B74FDCA849","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f39bd4d9055f68d914eada26b09dbdb8ce205c2","datavalue":{"value":{"entity-type":"item","numeric-id":4874652,"id":"Q4874652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bc852c41f9bcb267c4c0645cd985da87dcd2c44c","datavalue":{"value":{"amount":"+0.87056494","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$47A2AFB5-56AC-42A6-BF99-B22F01E3F953","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"570234ba6ae1c640f1df052d5503993d79ed0c7c","datavalue":{"value":{"entity-type":"item","numeric-id":4007589,"id":"Q4007589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ade497a11bd493d8e2e3ee9d23ab7a9791c18b7","datavalue":{"value":{"amount":"+0.86059797","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$FFDBAD99-28E0-4B6C-861D-61A1B4D7ED72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e90f4c6b26a566a68b1040d6cf1cad160b8f7458","datavalue":{"value":{"entity-type":"item","numeric-id":1276509,"id":"Q1276509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5bde045ad839db2729bf003d1e228ebdfb180ded","datavalue":{"value":{"amount":"+0.8585111","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$D6C56DA9-0EF5-4EF9-ACAE-E16E0912B238","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"42e107e97762adc8e9195fa73b250b28c0481a43","datavalue":{"value":{"entity-type":"item","numeric-id":4020487,"id":"Q4020487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bc5b643bc0fba00b3531f6532b44e639822c354","datavalue":{"value":{"amount":"+0.857758","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$5A64CB1E-8565-402D-B813-CAE885FF3CF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01e6f0886f191f46c4c17f4efe7bcb1d13fca3e6","datavalue":{"value":{"entity-type":"item","numeric-id":5898909,"id":"Q5898909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9555bfa9e3d13d3db66ffe1db8fcb0e461f2b9a5","datavalue":{"value":{"amount":"+0.8528002","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$8E2D851E-D8E8-40B7-B8BC-0653C7D9E1B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52ba5bcdc2350007ef56b9224e042c7d7576c344","datavalue":{"value":{"entity-type":"item","numeric-id":1825945,"id":"Q1825945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d68015654d76e37f22e62fdbc9cb018bd561f460","datavalue":{"value":{"amount":"+0.85208505","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$24780987-E4F9-4656-954B-BDDBE1D6D892","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8996216f3a8c8f6679a40d27d7d6a6d203a26a54","datavalue":{"value":{"entity-type":"item","numeric-id":5526125,"id":"Q5526125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31f93069b2e1a01cf49f96c621943b4e144e7af6","datavalue":{"value":{"amount":"+0.8516326","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$FAD6AF65-864B-42F1-9DC8-22597006BEB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b3c4d5ed75c3eac6e204b8dd838123f665867f9","datavalue":{"value":{"entity-type":"item","numeric-id":2333674,"id":"Q2333674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecbbb6b17f989570bb70ffcbd29af05b99636136","datavalue":{"value":{"amount":"+0.85094905","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q386032$5A8C4E03-8209-4649-A151-74B442D2417A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A mechanisation of some context-free language theory in HOL4","badges":[]}}}}}