{"entities":{"Q2280212":{"pageid":2290955,"ns":120,"title":"Item:Q2280212","lastrevid":73028616,"modified":"2026-04-14T09:30:29Z","type":"item","id":"Q2280212","labels":{"en":{"language":"en","value":"Milestones from the Pure Lisp Theorem Prover to ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7144307"}},"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":"Q2280212$077CF1F9-9061-4C6F-B185-61FDBC3CCDBA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3375baf833a5a66bc3ddd857e57dc8e6aa1bc34c","datavalue":{"value":{"text":"Milestones from the Pure Lisp Theorem Prover to ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2280212$95FA5A35-F27D-412F-9764-E218CA2BE898","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fee8ba681fbcc2538506240621b3ead57d36dfb8","datavalue":{"value":"1427.68348","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280212$41556CF3-1347-40CE-B634-8989212FF974","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$C6019FE5-3DE9-47C2-B162-5433B47FBCAE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2f6772b50db402e319131e91836e24f594dd3ca2","datavalue":{"value":{"time":"+2019-12-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2280212$7FBE6A96-BE77-4A3A-A870-D8A43CFBB020","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280212$0BE3A572-B329-4F16-86EB-A101B02CFFA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"540259e42205310d3310d3dad9dbe9ae50303b84","datavalue":{"value":"68-03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280212$050598AF-8BC3-4265-A22D-F805C35BEEC6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"da7da623c91d83d7bc715d38b056f925df1ebaa3","datavalue":{"value":"7144307","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280212$E08BBB51-E795-495C-B157-BCF981CC974F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$564F539F-F8B3-4233-8B87-5A1EE566BFCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3984bd10748b892f99d0b2a37906d069a5afc53e","datavalue":{"value":"hardware","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$7D60DE21-53F7-456F-B1AF-61043CF6888C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d71507f2ed2edacf3bb5d42233bf1a178a69b919","datavalue":{"value":"software","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$C2DBFE1A-29B5-47E7-B89D-2F1A08256E8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$05E760C5-0551-4BAA-A137-E1981A763108","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00b76a2e54f8798fe172effecd557ced03e2f904","datavalue":{"value":"functional programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$D28E66C6-47FE-4DD6-A7B4-6E67C18E4955","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"438a215c5cd761877e86d4291eeff2dfc5116c02","datavalue":{"value":"Lisp","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$5EE48D68-B3D9-4CD9-8387-FBB1BFD3C741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa8a6101ff90bea77f851517b5a991ddcaf7286b","datavalue":{"value":"induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$702DE7BB-A31B-433F-B49D-A4F2DCDA4F3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"476e70cc5d552d5cdc76575cc73d40a8bfb4b86e","datavalue":{"value":"rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$D147F464-E665-4BCF-8C0E-812DAAC163AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50b1882775c4720c2bd9796b439d3fd05a08dcd3","datavalue":{"value":"reflection","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$B58C1123-C887-4E8B-80B2-8C24893C9731","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280212$FA331121-DA93-4AE2-B553-42E1D38DD722","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0d384413a2d1b8185eb46b74e5b2c74244e0aac","datavalue":{"value":{"entity-type":"item","numeric-id":928667,"id":"Q928667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$3D5F6BF2-5314-44CE-9F51-B547F49631A3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$59EF67A4-DD23-4205-BC43-EDC1E02B5D50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$992F1DCE-4EAE-498F-AF5B-A48E5881DE63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$37787DF7-F696-41BC-9514-070249DDDF88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3bb5b4f58bf0ec3fac40486f165ecbd4b66faf26","datavalue":{"value":{"entity-type":"item","numeric-id":44026,"id":"Q44026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$20315FAC-10ED-407F-872A-D04D82DC8368","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"068499b3a994d33d8ddd017e122d544fc5d97703","datavalue":{"value":{"entity-type":"item","numeric-id":44027,"id":"Q44027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$64A5B86A-67C3-4B4B-B6A8-B3D00DC57B5E","rank":"normal"},{"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":"Q2280212$C3A87556-7413-4050-B640-89D7E6C7A4D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$29BEA51B-75F5-4EB5-A904-3AE1713425B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$8A74B358-73F0-4BB4-8933-493471E5EE52","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":"Q2280212$0F1E100C-6233-433A-B7AA-B565715E5BAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8f057223c758d6b8295ecbdef4842faac2ccb72","datavalue":{"value":{"entity-type":"item","numeric-id":19253,"id":"Q19253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$DA280622-F50E-4960-9EDE-A97811857802","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e751138e8b150b28783c5a210048f6817120432b","datavalue":{"value":{"entity-type":"item","numeric-id":32511,"id":"Q32511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$CCFDCF00-1496-4B1C-9078-D0874BA114FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$28099D75-0A6A-4F3A-8204-4123BF698E60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e079f4640d565f0ca1930fd327c2c7e8d634508","datavalue":{"value":{"entity-type":"item","numeric-id":21954,"id":"Q21954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$F35136C8-68EB-4C1E-A2F0-8204E3AC284B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"44e192ea0614ca90dcab29c306f09db708056c50","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$7FD0F02E-3A4B-496F-A9D4-3BC966C7D2D2","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":"Q2280212$8400D1D3-1ED8-49A1-8E9C-F3F869A67E1B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"da7c2802e385fab852f6ff750769cd41594e0c18","datavalue":{"value":"https://doi.org/10.1007/s00165-019-00490-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q2280212$E22D2190-4C31-4E7E-BBFA-36107D85EE98","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4f0598757b36f83cdcfb5446366eeedfe952041b","datavalue":{"value":"W2964806919","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280212$4A325F3F-6083-4FD3-A558-25B8EC400213","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"280442ce105b23ca3597e15fa2038c58314d7165","datavalue":{"value":{"entity-type":"item","numeric-id":1845619,"id":"Q1845619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$B1B7CC3B-12D7-4248-A187-743CD3E92BE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"283b457c1aa928df8cba388628638010a8a9e043","datavalue":{"value":{"entity-type":"item","numeric-id":4016540,"id":"Q4016540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$41FE9AD9-44D7-4CFC-8D54-C6099647C503","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f20e02bb907f90cb22a0a676f448fd7139f7410","datavalue":{"value":{"entity-type":"item","numeric-id":2547495,"id":"Q2547495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$43FB914B-4079-425D-BA11-058442999FD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cf4bd6f65936497199af77b410cbe7fc34d2615","datavalue":{"value":{"entity-type":"item","numeric-id":5663380,"id":"Q5663380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$CFC4BF00-C86B-4D49-B3D5-DD30735EDC90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"527c7202e783b352edb1e0158278fe604f9a2b5a","datavalue":{"value":{"entity-type":"item","numeric-id":4105761,"id":"Q4105761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$FE9ED152-9610-4293-8A94-2AD928B33D37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74e200c4f897ac4cb0c5ae9f1bab6477c1d7e3dc","datavalue":{"value":{"entity-type":"item","numeric-id":3090391,"id":"Q3090391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$EAAA58C7-3B7A-49AB-BB41-9668E2B29730","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":"Q2280212$AE1860A4-91C1-4053-A25A-5DCD50D9176A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bce4f5ae886a6add198cde1454a758dfcc3c40fe","datavalue":{"value":{"entity-type":"item","numeric-id":3932277,"id":"Q3932277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$EDBB6F72-6471-41D9-A401-939DCFA01A69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df99d010c323d1ce4719d0c5115c3a289e30a204","datavalue":{"value":{"entity-type":"item","numeric-id":1107510,"id":"Q1107510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$DC96CEF9-FEDD-4446-A655-B2AE402FB700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$294778BE-1E61-443E-8DE6-9B3E76A715DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7eb3e97929024d2ee37616602a13d3244533bbb2","datavalue":{"value":{"entity-type":"item","numeric-id":3835049,"id":"Q3835049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$BCBF0A2C-D31A-49BC-AE55-74ECE4030C11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b63e4e6e8c92ebfef6844c6464a49c0beb008a05","datavalue":{"value":{"entity-type":"item","numeric-id":3000661,"id":"Q3000661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$843E1CBA-6F42-426E-9630-599BAB20AA32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5ccea7b6fe9f5a7082344f9edaface083da76","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$E843A5C5-2556-4FE6-9FFE-A1F8A27C42C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcd44752aa5df5cd038054d2d30c6001d6392b03","datavalue":{"value":{"entity-type":"item","numeric-id":286790,"id":"Q286790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$1610B4A1-463C-45BF-A4BD-A045C3E94C1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff1c9576a9af1e44009a9ef9a0f7f22e091829d5","datavalue":{"value":{"entity-type":"item","numeric-id":5610986,"id":"Q5610986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$4EC38A3E-E1A6-4317-AA5E-878CD0F24470","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":"Q2280212$2294369F-61D8-490E-B04A-85E01B3A6528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39504f8c7c18a19dd2bc2917fdd5108f9b807c6e","datavalue":{"value":{"entity-type":"item","numeric-id":2754047,"id":"Q2754047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$4A8251D6-3616-4C79-9FCE-A523842E6328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d43182de98d159f0ebb543c5126e0ae385036ba","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$AA2692DC-F11B-4A11-847C-E7136DC99AE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64fb3e8e1bce2eac8344ce1eacc6de3a8144fcba","datavalue":{"value":{"entity-type":"item","numeric-id":688572,"id":"Q688572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$7E9BFBD3-E822-4E43-8C1C-4EA1990A07BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba2e9956e014ae28c735471b8fe8bc11ac76e0c0","datavalue":{"value":{"entity-type":"item","numeric-id":5670164,"id":"Q5670164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$017BD4A3-6BD2-4F8C-A58B-D2A160CFF4A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dbf5d4c6cedd5848e03816494729378cde53a8e","datavalue":{"value":{"entity-type":"item","numeric-id":2551698,"id":"Q2551698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$112A350D-A675-4754-B005-8605397C446A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71bcd874c7237a1b9de1d785ccae342680b949f8","datavalue":{"value":{"entity-type":"item","numeric-id":2303245,"id":"Q2303245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$15BAC570-E522-4D4F-AE07-BAB991128A9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a49cfd6942550ad4a0d31d13bbc5815a4eee0ee","datavalue":{"value":{"entity-type":"item","numeric-id":3154457,"id":"Q3154457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$519B868B-629E-4B25-9816-E0F6911F1481","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4eaf43a88b14444f4a8e2ab2282321b709bbbae3","datavalue":{"value":{"entity-type":"item","numeric-id":5601829,"id":"Q5601829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$0F149A8A-5A40-45A3-8755-8CAA785F4239","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f2acd13394e12d53f7294c47790565e27a57f11","datavalue":{"value":{"entity-type":"item","numeric-id":3857731,"id":"Q3857731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$27384F21-1FB7-47A4-9944-C56E59F30BD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01cc0603799551d88cdcf60c08da4c96b4eb1c0","datavalue":{"value":{"entity-type":"item","numeric-id":5900722,"id":"Q5900722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$72F0DD12-B4AE-4A65-A8EE-06DC96A35F30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$C64AC728-C7DD-4C99-BD68-1F29ED73C33D","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":"Q2280212$6E1E5BDD-05B3-46B9-8A78-0DBB65370699","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$DBC0334A-1C3D-44CB-8280-CFF090E9B39C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7493bf656ba59564acd6b7893d63e8087a65415a","datavalue":{"value":{"entity-type":"item","numeric-id":3960818,"id":"Q3960818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$B62051E8-C0E1-4050-AD56-65D1BC654BCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"daa75d76e1cdc609f7ac46974607202a4c628e1e","datavalue":{"value":{"entity-type":"item","numeric-id":3275832,"id":"Q3275832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$2D60E9C2-B684-4EDF-AD78-753F24B37473","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39d1d8fb42339a481de309d10a4b5b6fb7e49eec","datavalue":{"value":{"entity-type":"item","numeric-id":1140436,"id":"Q1140436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280212$9A5F9713-F0BF-46B5-B5FB-BA3E9863AFAB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"975bbf58a6cd3cef220fcb8b373a0c1f21aa27c5","datavalue":{"value":"10.1007/S00165-019-00490-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280212$7656EEB5-E1F9-438E-B598-55E2D4EA58A3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9c7e2906cab0df39eaaaec6ded4334d15f17931","datavalue":{"value":{"entity-type":"item","numeric-id":4471942,"id":"Q4471942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea9419248afe97b6ead735f0c58b0e0f89241e52","datavalue":{"value":{"amount":"+0.8603591","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2280212$4B3968A7-C9E7-4432-A37F-E47042B5552D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56d606835397ced889225aa24646e03238343394","datavalue":{"value":{"entity-type":"item","numeric-id":3000661,"id":"Q3000661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4a946bd49d9e81d2edde85a75b778600a2556a6","datavalue":{"value":{"amount":"+0.85202587","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2280212$159CEFBD-3D28-4D1E-9A3B-66A7A9576A5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"067b9ee5d1759bf8dfdf5a7d76851fcc9c0894c5","datavalue":{"value":{"entity-type":"item","numeric-id":1610218,"id":"Q1610218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4de840d469674b2ecf12892d3b208e2d00ec3a5f","datavalue":{"value":{"amount":"+0.8509307","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2280212$4BAC8FF7-AEC1-4D9E-B0AD-A8445965B00A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6e02866bedcdddc38a6d5d0dc3312cefd57e45a","datavalue":{"value":{"entity-type":"item","numeric-id":2870142,"id":"Q2870142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72f0125dc289422aaeb1a232d3c5b7a423db52b9","datavalue":{"value":{"amount":"+0.8497652","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2280212$0DEBCC37-8195-4F8C-B6BD-D010BFC5E7AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14e60829bb710e6304c124f9db7c3007a450cd88","datavalue":{"value":{"entity-type":"item","numeric-id":5088166,"id":"Q5088166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c0d8bd3fee7a014890a6167354ca8eb7dbd430d","datavalue":{"value":{"amount":"+0.8484997","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2280212$6BCDDE45-DBC9-42CA-882E-21919AA88E30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80b1e46e45aa8463186c712b3d0f19a26cfc2187","datavalue":{"value":{"entity-type":"item","numeric-id":5428255,"id":"Q5428255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5bf9d0ca1886f49352c566ceaa6297d87435c502","datavalue":{"value":{"amount":"+0.84785604","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2280212$0C0B93BC-FE84-4BA7-B925-53368EA4C83B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7fb1101926584588629995559670ee57c402e54","datavalue":{"value":{"entity-type":"item","numeric-id":2642461,"id":"Q2642461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1aa33060ef14ff9c509770f07fc801133b754bcc","datavalue":{"value":{"amount":"+0.8447299","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2280212$98E58BB7-7175-4D4A-8284-67EB5E3DCB8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9f875caad3248ec793d0a44f3a47ce79c6f08ae","datavalue":{"value":{"entity-type":"item","numeric-id":5088168,"id":"Q5088168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"010cf729976974a28ac5d166cc496613ba848a9f","datavalue":{"value":{"amount":"+0.8437612","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2280212$EC922DAA-3FEA-40CE-AC11-106810051844","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Milestones from the Pure Lisp Theorem Prover to ACL2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Milestones_from_the_Pure_Lisp_Theorem_Prover_to_ACL2"}}}}}