{"entities":{"Q469367":{"pageid":471134,"ns":120,"title":"Item:Q469367","lastrevid":62149008,"modified":"2026-04-11T04:05:50Z","type":"item","id":"Q469367","labels":{"en":{"language":"en","value":"Applications of real number theorem proving in PVS"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6367494"}},"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":"Q469367$EFD6258C-83A3-405F-80D5-D1B15A880B70","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2d117137091bd28ca3e1c1ad47264863fca09c68","datavalue":{"value":{"text":"Applications of real number theorem proving in PVS","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q469367$4003C8B0-C3F8-4FBC-B139-3AF93A7A9A5D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4e5c14343428e1004da4680e7a882bfcd7694446","datavalue":{"value":"1298.68252","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q469367$EFC100B3-845A-4076-9FE6-E92D9FD4E03C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cb9b93568be1c0bebeae1e5d93b7237313ba15d","datavalue":{"value":{"entity-type":"item","numeric-id":469364,"id":"Q469364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$47F045A3-8FE0-4BCB-8EC3-16EE0B6C4486","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f88153ebb812b5dac758543e6209287fc145755f","datavalue":{"value":{"entity-type":"item","numeric-id":469365,"id":"Q469365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$9D0077DE-786B-4D9A-9383-D5402C6A3691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"267b5127dd44070b65d70ba69064cb6fb816c8f6","datavalue":{"value":{"entity-type":"item","numeric-id":469366,"id":"Q469366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$2CF9F066-644D-4825-A9D7-065F98FAF175","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5b182cd4f9e9cb54195b7976a497640f4d81f2eb","datavalue":{"value":{"entity-type":"item","numeric-id":1169557,"id":"Q1169557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$559A2874-6964-4929-A880-CB781DB9C7A1","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":"Q469367$0160EBF3-C6E9-4003-B5DF-AE8C371EE23B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2cc33ed3b977d25c716db29b5ad1f5456ca00b73","datavalue":{"value":{"time":"+2014-11-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q469367$B43050BC-D2CB-41C9-93EB-CA6F4E639B5F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q469367$FF212527-1E6C-4178-84B3-4AE5E9D5D1E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q469367$AE1F62FF-2B0B-456A-B02C-3473DBA13E44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c9727d9ee90ef6c0f1bdf0ba5bb711e9a6b7cd05","datavalue":{"value":"93C95","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q469367$CDAA94DA-0D4A-4254-88E1-3729EA7E02A4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6493591767378c1cf51420c654a9eb0382616037","datavalue":{"value":"6367494","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q469367$2C2D071D-80BC-47F3-A9BE-4ADEA33E744F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c7a035490732e1f929b80db9f18f857024a9350d","datavalue":{"value":"real number theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q469367$F35540B6-C0FA-4897-93F9-6F1BAB86D0ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q469367$E3C7B51A-F50C-423A-A7A6-5455E814078E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c69974b8ee44ba9ffc58b48877209f3953502907","datavalue":{"value":"Maple","type":"string"},"datatype":"string"},"type":"statement","id":"Q469367$6716195E-A1CD-4494-89E1-D83B2DA9877B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a873697bda241540e1019f29607482dad4f3a700","datavalue":{"value":"control systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q469367$F6DD2D71-221C-4A13-8317-9D5A98E86CFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2348fddce5548ce2f897e03fe909420d23858fce","datavalue":{"value":"test suite","type":"string"},"datatype":"string"},"type":"statement","id":"Q469367$7B607137-03CE-45D3-8133-C2AA959C72BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a90b155a4e032aeb50fd1d69720eb778dbb0fec0","datavalue":{"value":"air traffic control","type":"string"},"datatype":"string"},"type":"statement","id":"Q469367$D563B3B8-2627-4B07-B318-12BC3BE754B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"77aa72471018a9d9d8b8f6e40ef7a72d89a92c2d","datavalue":{"value":"higher order theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q469367$12B122A7-D4A4-4DFD-857E-8FD7D5236BB2","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"3fe634e17b3ff74634b48c40286b514dc1f69f6d","datavalue":{"value":"Q55393267","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q469367$CFF421E2-1A90-48FF-8E86-68CD9FD49E1F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bf8fe40ec0751f683b8f31fdc6f7f38f8aa07409","datavalue":{"value":{"entity-type":"item","numeric-id":13328,"id":"Q13328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$F07DC3D5-B45B-4E12-8185-0C196C55854C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$F1045A6D-3B61-49BB-8FD8-DBC0E8D733FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3c22b4e6c24037f313b1837c22cc6ae0308a77c7","datavalue":{"value":{"entity-type":"item","numeric-id":13503,"id":"Q13503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$24938AAA-0E09-4AAB-8F9B-E4413441C17D","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":"Q469367$92118340-E04F-4E84-8AEE-76B942B445DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"02d32efa4caa2abb72a4e6348351cc4a9bcbccbb","datavalue":{"value":{"entity-type":"item","numeric-id":16527,"id":"Q16527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$3333E7BD-FCD7-4EB7-A02B-548BE318047E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"66eb045e037081b6f6e8499f9fef44d8fbb7e0b0","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$BD4C80A3-2AC5-422D-9B19-FA5CE2CD1DBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a709ac7c97c67049e241e0b036253f1d955c589a","datavalue":{"value":{"entity-type":"item","numeric-id":13313,"id":"Q13313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$8DAB2AB1-E43C-46EA-8739-2484A4F3BCB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"485f54a0549a89232924cb0abb443c2fad36af9f","datavalue":{"value":{"entity-type":"item","numeric-id":13300,"id":"Q13300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$F5EFF53C-7430-4B39-B595-2C158399AF5D","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":"Q469367$F23510AC-1265-4F7F-ACCD-4C56A39D8AAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ac15ee65d13845f30d32328a0a6e9e525328e3d1","datavalue":{"value":{"entity-type":"item","numeric-id":20725,"id":"Q20725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$BFD5C54F-0179-4022-988B-52F687C2F3B9","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":"Q469367$1CABA012-5321-4F71-A922-655AAF52F698","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"540c378922133e97da9190bd94e3405dd2dac269","datavalue":{"value":"https://doi.org/10.1007/s00165-012-0232-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q469367$10FCDD29-FABE-447A-A46A-52B8BA083692","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7b97f2f6932b6d459b5cbdb50ad3e1bf473961c6","datavalue":{"value":"W2074445571","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q469367$2F8044CD-0548-4619-BF7A-50A66A99996E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7714e08a8556aa1cd6a9f5fda8c7d4f8d9c37ba9","datavalue":{"value":{"entity-type":"item","numeric-id":4790649,"id":"Q4790649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$76A7176D-6E72-4685-A941-89207190F86C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f72f65644d666e389907b7173225cdf0065502fd","datavalue":{"value":{"entity-type":"item","numeric-id":4571480,"id":"Q4571480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$0F8C59E6-31D5-4FBF-B0FC-7DD4418C2538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0c823d8e6210b74fc0c9066b9f78413cf1f33a0","datavalue":{"value":{"entity-type":"item","numeric-id":4263160,"id":"Q4263160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$E0C287F6-0E84-498B-A024-2087FCBF72DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2db59ebe3a60ffa67aebe624b413e10df05b585e","datavalue":{"value":{"entity-type":"item","numeric-id":5505501,"id":"Q5505501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$F1DB2AAA-F8F0-4E69-9CDA-5BA5A4195A6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0d791a34db49852ef4e0279239cd68ced434ed9","datavalue":{"value":{"entity-type":"item","numeric-id":5520081,"id":"Q5520081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$74FD62EB-3F8A-4B79-8313-F196AD142B85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"017dca64578e6979a09aeeb8b382b1388bace1b7","datavalue":{"value":{"entity-type":"item","numeric-id":4810199,"id":"Q4810199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$40D2E1C6-51A0-440E-92B4-767A11D6B0E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19121fe5036f2676946186c6f9a088bb5b461d0f","datavalue":{"value":{"entity-type":"item","numeric-id":4227289,"id":"Q4227289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$0B5DF039-1180-4739-AEE8-00D621128D7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7efc89b00747c2007ed9ade9adc81ef9eff5327","datavalue":{"value":{"entity-type":"item","numeric-id":2754035,"id":"Q2754035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$5E2C43B8-EF6A-4DAA-9F29-4FD124F9FCBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9ad1ca0c030444e5bd3d91e22695ff17d7ccef1","datavalue":{"value":{"entity-type":"item","numeric-id":3898534,"id":"Q3898534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$AD9D5F0E-FE7A-4BC8-A31C-02BAB9166A9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"545b70a52fbd739fcbdc5fb79649e5d3315f9433","datavalue":{"value":{"entity-type":"item","numeric-id":3598006,"id":"Q3598006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$DEEF873B-1601-4B71-B457-E18F21AF6B9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aaf6187ca0a713a5be48fa8bdf70e7de963ab3d5","datavalue":{"value":{"entity-type":"item","numeric-id":2769090,"id":"Q2769090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$88E15BCA-4431-4824-B658-1DE83B721C6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"874f49a372f928bccb4bd697306995ca958352b9","datavalue":{"value":{"entity-type":"item","numeric-id":1578436,"id":"Q1578436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$111C4DE3-20FD-4A2D-BCE0-B0F96F25F2AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$D9012EF0-950E-45CA-8C0F-FDD5DA070716","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3c3bf718886c6e11599d9273e2bb7aa3c293801","datavalue":{"value":{"entity-type":"item","numeric-id":2754046,"id":"Q2754046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$85A1A196-F759-45C8-A649-0D87B07982DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"552c0fd0688cc1cd0d242c6ea1573c9e5fd80831","datavalue":{"value":{"entity-type":"item","numeric-id":5477656,"id":"Q5477656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$B937E23B-3DEA-4907-9CB9-5021E9167E8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"865c08315029ce56b657c49ca7102fe1d09d55d6","datavalue":{"value":{"entity-type":"item","numeric-id":4003780,"id":"Q4003780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$8AF776EB-F40C-45EB-BA25-DF4B7A15305C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68c91066f858fa64a799af591825e0694228fffb","datavalue":{"value":{"entity-type":"item","numeric-id":4122841,"id":"Q4122841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q469367$14EBED32-E440-4BD5-B10F-23DD8A57C208","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"28612739994dd6c23f920e1178d63ab8eeca116d","datavalue":{"value":"10.1007/S00165-012-0232-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q469367$2B38EED2-B871-4FEA-9B46-AC68AFE8362F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11bdae9f731c0e1145ebd1c0e2604117a0993d0f","datavalue":{"value":{"entity-type":"item","numeric-id":5477656,"id":"Q5477656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8ec1e4420ca627170c1c3935178454fe7911fc2","datavalue":{"value":{"amount":"+0.7651785612106323","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":"Q469367$9017A643-9EB2-426B-8C75-442095E700B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8648fefe25b990ca49378b9d175a37f95f66e4e9","datavalue":{"value":{"entity-type":"item","numeric-id":3543660,"id":"Q3543660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"afc9f2ff4f509ef3806a564c6eccfbdd27cedfc7","datavalue":{"value":{"amount":"+0.7605475783348083","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":"Q469367$26D4EC47-0EDF-4CB0-AA92-F3BC70F857E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e13f94efa5a180ee860e2173b41929c73d33793f","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0234079f06c3d5a2de92e81729db92b1040d50c5","datavalue":{"value":{"amount":"+0.7441164255142212","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":"Q469367$01161088-7F07-405F-84B9-D361CCC4BA50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24c4e1af29df48aba6865efb69804492ca54b4af","datavalue":{"value":{"entity-type":"item","numeric-id":2703760,"id":"Q2703760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5151cd5c073e690d53241015bc1ce97f4ce535f","datavalue":{"value":{"amount":"+0.7374658584594727","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":"Q469367$2B67EC07-699E-4572-BAC3-7EABDFEF8E6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2741c52220bb969f7227380e5961fee06f2cc5a7","datavalue":{"value":{"entity-type":"item","numeric-id":264193,"id":"Q264193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8707c95cb40d9f0e82e4fa308ceb56ffc42a267a","datavalue":{"value":{"amount":"+0.7240477800369263","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":"Q469367$BC349E1F-8092-4045-896A-7E35FD240497","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Applications of real number theorem proving in PVS","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Applications_of_real_number_theorem_proving_in_PVS"}}}}}