{"entities":{"Q5956117":{"pageid":8132919,"ns":120,"title":"Item:Q5956117","lastrevid":47745673,"modified":"2026-01-02T14:22:42Z","type":"item","id":"Q5956117","labels":{"en":{"language":"en","value":"Nonstandard analysis in ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1708525"}},"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":"Q5956117$040E0D67-F656-4D20-8DC6-6B0D5D2D4872","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"472e8b09c11141c0b495352b5286f60b31d4c1c8","datavalue":{"value":{"text":"Nonstandard analysis in ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5956117$84593025-2013-4D4E-BFDF-88B18DE3DCCF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1361d9e301d330512c8d0ed0d410b8758f424f71","datavalue":{"value":"0991.03018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5956117$48AF1B21-FEA2-4B5F-8825-B1E58BD09C21","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d2aaaaf5217c57f1c0a2dd9cc6bafe7110c94ca6","datavalue":{"value":"10.1023/A:1011908113514","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5956117$B2F534A8-7ED9-4BBB-BC4D-697AFFBBC1EB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"53de145c1476af14e05c31ec8165f08e3c85436f","datavalue":{"value":{"entity-type":"item","numeric-id":230813,"id":"Q230813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5956117$3DB9B574-94F9-45C8-99B9-1EFE7A569BBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5956117$509DA250-152F-44F5-A84F-A05D10F5707A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5956117$5EC95047-4308-4A99-B73E-6032A4E172B9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0bd22e9bdafff3cc4af9c050513c24081452898e","datavalue":{"value":{"time":"+2002-02-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5956117$73DBE229-B336-4DE5-8ED3-E1D21CCDDA3E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5956117$BDCE2B89-D487-4B71-959F-854E92E3AC74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5956117$2916E91F-9C79-4923-8644-79972B192D44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6db4aec5ef7fbf0e828c6d2589c9166d8caea5c3","datavalue":{"value":"03H05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5956117$8A29B846-5FB7-4D4A-BAEB-786D75ABE81F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"99f9a71a74d1df394756dd769a7c52debca7f34c","datavalue":{"value":"1708525","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5956117$70EFE0D3-3AC4-413A-8A75-257977969DF3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93870bea9e95850a8c2c168e966ba73051e6fe83","datavalue":{"value":"real numbers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5956117$05379400-0D13-4F2E-AAAA-26078E54503B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f99c0228893afedf64c8268c7d13b899d294fd7c","datavalue":{"value":"complex numbers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5956117$FD21011D-F6DD-4E91-9AA6-AD09057EC786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d55c9a2c4b34db2848066ec61b5803ef53a65298","datavalue":{"value":"Common Lisp","type":"string"},"datatype":"string"},"type":"statement","id":"Q5956117$55FF662E-1D66-4111-96F2-8C5BF6BFDA9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5fbe3c7285c82b7e85a0384689c42c38ba7418e4","datavalue":{"value":"automated theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q5956117$F3E35D8B-AAE6-49EC-B25A-C350D74BB1F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24dd5926fa2c4f0ee181b086899e10f05b3e9148","datavalue":{"value":"ACL2","type":"string"},"datatype":"string"},"type":"statement","id":"Q5956117$D82D9BA6-6F83-4333-87AE-641755AEE1A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"167dc8bc8963b3df05b7ff9ad19961d33d38408a","datavalue":{"value":"irrational numbers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5956117$EA9DF376-B33D-41A6-A46E-C6E18D81520C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a11cf132947b7b29693c82a290ecbf2e4989b042","datavalue":{"value":"nonstandard analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5956117$0AE23794-E3EB-460E-BA8C-BB21B26D4B38","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":"Q5956117$A84FB75B-D2EB-49A6-9973-40C2ECD028F3","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":"Q5956117$DF0BC0EA-AD8B-4CC0-BD5F-2CDD75A4D012","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5aa5977f6d43f54d5eb00b2aef6e369e713dd699","datavalue":{"value":"https://doi.org/10.1023/a:1011908113514","type":"string"},"datatype":"url"},"type":"statement","id":"Q5956117$44651F4F-276D-439D-82AD-D9CECD3BF8AE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"05c72946c84dfc62709e20f2fd5147ee6786c366","datavalue":{"value":"W1542193405","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5956117$E17C345B-EFD5-4801-B4EC-474C70690FD8","rank":"normal"}],"P1643":[{"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":"9a315d92a18d44ab33292ed474acfb22e807cb71","datavalue":{"value":{"amount":"+0.8805520534515381","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5956117$0D6721D2-612B-4961-A714-FC5D99C042BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ec9048f0c16019dacc5a2b0ff53606251c8e48b","datavalue":{"value":{"entity-type":"item","numeric-id":5897076,"id":"Q5897076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f37f1e6e538b2de788f813c06b736e1da7406b12","datavalue":{"value":{"amount":"+0.7492256164550781","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5956117$5F0FD6B1-7657-4DFE-B07F-67B3E3C3C52B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"afb714d42d44aae2ccfbff437eb23fd0a25261c1","datavalue":{"value":{"entity-type":"item","numeric-id":4504968,"id":"Q4504968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d4a22ff5a9aec82ba3b4a1d491ae8cfec48dbc2","datavalue":{"value":{"amount":"+0.7406779527664185","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5956117$AE937D95-0E27-4C26-9456-6829CD363323","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2ab816ca20d777bf64b417cd94a39c25aff51b17","datavalue":{"value":{"entity-type":"item","numeric-id":4817211,"id":"Q4817211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc9172d95dd1c61c14cb6421c066fbffa12cdc38","datavalue":{"value":{"amount":"+0.7387498021125793","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5956117$50BE91D3-5969-4A66-B31C-BA13B3524DE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52785f2dd2003261c737010c9dd8c0d12eaa464a","datavalue":{"value":{"entity-type":"item","numeric-id":1334896,"id":"Q1334896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"344c70b01f13bd06ad731a1e9ed56c293475d028","datavalue":{"value":{"amount":"+0.7355350852012634","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5956117$EC141347-B6C3-4D45-8D4A-94B129C9BE33","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5956117","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5956117"}}}}}