{"entities":{"Q1426938":{"pageid":1437678,"ns":120,"title":"Item:Q1426938","lastrevid":70377102,"modified":"2026-04-13T14:22:03Z","type":"item","id":"Q1426938","labels":{"en":{"language":"en","value":"A mechanized proof environment for the convenient computations proof method"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2057415"}},"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":"Q1426938$2A980392-E914-4B51-9ADF-21C300205353","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2a07c2c58c0c075b3395f03afb3f1c96408e4aee","datavalue":{"value":{"text":"A mechanized proof environment for the convenient computations proof method","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1426938$17FD10E9-0F6A-4955-867E-8CB4D3C88E1C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6b3aeb6adfb3a2e8ae52fe298d9b02a8bb3c6deb","datavalue":{"value":"1057.68111","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426938$389A2A4A-0859-4877-B610-78113F1531B4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0422388fed092f3a036bbee7b591c4dc65b5af80","datavalue":{"value":"10.1023/A:1024746015231","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426938$CDF2DE54-012F-46AF-847C-4E67DF67F28B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"718558337bda92b321cef97da5da3049e8378cea","datavalue":{"value":{"entity-type":"item","numeric-id":1426937,"id":"Q1426937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1426938$703D9E7F-03ED-40A0-997B-D497D0934F65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9568a61c55802ceda18ea5e885b2fc3da9204e0c","datavalue":{"value":{"entity-type":"item","numeric-id":340039,"id":"Q340039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1426938$62B28BD8-619E-4F84-8DA0-7D166865FBFF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1426938$0D568953-A2A5-40D8-A6C7-E3D7264B0C52","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"47829e28918d048336111de08a0f0c93aec92d0a","datavalue":{"value":{"time":"+2004-03-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1426938$F76A5A67-2840-4364-B61B-0B44416818B9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426938$A5D213B1-D5F2-47B8-9718-06B0EFF07DBA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"edf8c34f6c60bf0d21423a21e5c838c120c6a2ed","datavalue":{"value":"2057415","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426938$0566042C-466B-4B8C-A8D1-FF5EDB95DDB6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426938$8A75D97C-DAF0-4271-AB81-5039536DEB01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b7c584610c89bcae17bc84a44cbc0a7885373532","datavalue":{"value":"convenient computations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426938$B2FF1821-66BD-4EA7-8D57-835AF0E1EDCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1309ae3232c2119ec80eecff6a6b410fe312aabf","datavalue":{"value":"proof environment","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426938$113E51FC-C653-4564-AD07-92596D2F5D12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426938$E9DB8204-1058-414B-A535-911761D290D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c28f0613ac069d717c563bb2b7bb74d41aed6844","datavalue":{"value":"deductive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1426938$9E2D7ADB-BC79-4AA4-A1A5-F67FA080B863","rank":"normal"}],"P1463":[{"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":"Q1426938$5E44B26D-6D07-4E0F-B236-5E55143AFB05","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":"Q1426938$E914D8A7-B965-431D-BB41-02D3B555B762","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fb7a82de265cb379610d69c413374085a785ee90","datavalue":{"value":"https://doi.org/10.1023/a:1024746015231","type":"string"},"datatype":"url"},"type":"statement","id":"Q1426938$25C1F6A5-8BDF-47CB-866C-D387C3C58A15","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f9b8468e5ea40ef52dacf9f6ca10e8761e906e6d","datavalue":{"value":"W1605919360","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1426938$72CA43C3-1CED-4997-932D-106C12A7ABF4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de10203981c5068b0631b8004c64b7ff2f0e4f00","datavalue":{"value":{"entity-type":"item","numeric-id":4818803,"id":"Q4818803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"251820e4fa780bf0d09be5e8bf9648efb2a2a68b","datavalue":{"value":{"amount":"+0.8944185972213745","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":"Q1426938$1C52E41F-3C54-49BD-B534-D79B07A8FDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3c5d2633d7ccfe271a1e0af1c077b15f416c9ad6","datavalue":{"value":{"entity-type":"item","numeric-id":2729921,"id":"Q2729921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2aa963976eeb671206b5f029ddff4032cf69d98f","datavalue":{"value":{"amount":"+0.7044057250022888","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":"Q1426938$AC5F0B1D-A483-4313-B6EC-EBC9346DAB74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ff34c02a8377419aa6bc52038759eaf89019a2d6","datavalue":{"value":{"entity-type":"item","numeric-id":1203115,"id":"Q1203115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2c49a5a51dedf6545bb508d55860d3cb6f8126e","datavalue":{"value":{"amount":"+0.7032477259635925","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":"Q1426938$DEA5D04C-B1C7-42FF-9689-FB64E32E9A6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f74a4554d915abf3dc2af47a650d41ea7cdc430f","datavalue":{"value":{"entity-type":"item","numeric-id":3795197,"id":"Q3795197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b529eab2b2709055f973e3c8911a95bd68bbf93","datavalue":{"value":{"amount":"+0.6978647112846375","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":"Q1426938$78B1FCDD-ED11-43D5-BE20-8F320E30EB77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd49ed421a11de7a1f4822e888407a4ec83a9ec3","datavalue":{"value":{"entity-type":"item","numeric-id":5261501,"id":"Q5261501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b943b654e9d3599552dddba06396035eadce7a8","datavalue":{"value":{"amount":"+0.6915098428726196","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":"Q1426938$62151818-4BEA-481D-ACEA-64D8815E0CA3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A mechanized proof environment for the convenient computations proof method","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_mechanized_proof_environment_for_the_convenient_computations_proof_method"}}}}}