{"entities":{"Q4371519":{"pageid":6401118,"ns":120,"title":"Item:Q4371519","lastrevid":46990944,"modified":"2025-12-26T00:24:49Z","type":"item","id":"Q4371519","labels":{"en":{"language":"en","value":"Automated proofs of object code for a widely used microprocessor"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1105827"}},"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":"Q4371519$BF9BD19E-B44E-42B8-BEB9-D5E7348085A9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0f67bc1aac5d1d2f08980e5ff156b2e371101bc5","datavalue":{"value":{"text":"Automated proofs of object code for a widely used microprocessor","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4371519$CA2E2143-980E-4591-AF30-E6DB7CBAAE5A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"db830093d6c21dae779efd475c585d8500b4ed51","datavalue":{"value":"0882.68128","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4371519$7465EE59-AABF-4BA9-9AB1-2C7754827097","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2ec132e5ae2e5537e918435ef2ff78aa470c852f","datavalue":{"value":"10.1145/227595.227603","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4371519$F34A4222-A4A0-490D-B9C7-E09351EBE99D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"43c80439908def1f47a2850b299ced02bb922e89","datavalue":{"value":{"entity-type":"item","numeric-id":861688,"id":"Q861688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4371519$F6425214-8ACA-46BB-8E63-9128B120797C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3540fba49cd0198b0ed1d11b535ec985928b8c55","datavalue":{"value":{"entity-type":"item","numeric-id":525909,"id":"Q525909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4371519$8612A885-D6B9-420D-980E-53984A896D81","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f12bfc80fe4a431c556e028f5134a217234a7cc4","datavalue":{"value":{"entity-type":"item","numeric-id":63915,"id":"Q63915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4371519$AEAEAD21-F4BB-4023-A2C6-CB4B8ABD06AA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e923552579303fe8b30d2a139bb2fde0734b1912","datavalue":{"value":{"time":"+1998-01-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":"Q4371519$C165433B-8E5F-440B-AE2E-0DDF6B679CC5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"48a86c28032fa1c6d2fe2332380507de41c2e669","datavalue":{"value":"http://www.acm.org/pubs/contents/journals/jacm/1996-43/","type":"string"},"datatype":"url"},"type":"statement","id":"Q4371519$5AFDCA60-3B22-4D1B-AC74-2401E91956FA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4371519$E13BE220-60EA-4925-AB1A-9DFE1D307EF7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1005572ab83b624d2cb445045ab13afec27692fa","datavalue":{"value":"1105827","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4371519$32240166-2148-466D-8A1F-B5EE09DE0642","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q4371519$27A2C6FC-0E87-4AD4-851A-91A7CBB29D5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da9ac8f3baeb5525ec40e89c92b42400f315e3fb","datavalue":{"value":"Gnu Common Lips compilers","type":"string"},"datatype":"string"},"type":"statement","id":"Q4371519$AAA79728-7621-40D3-8427-D5A4D6D6B9E5","rank":"normal"}],"P1463":[{"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":"Q4371519$EEBA1DC5-790A-42C0-B09E-F3381BED46C9","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":"Q4371519$6F013F90-CE16-4233-8A2E-59937CF49282","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ae66a81ba7a3a5f9025680264e0bbb3e105facb9","datavalue":{"value":"W1965348053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4371519$FE21EF23-2B07-4C6F-A680-89B110B66185","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ffe8a18b6ca030aaa578fbb6b72d10ee81a2ec5f","datavalue":{"value":"Q130953892","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4371519$AFD3CD9A-A725-46EC-BEA6-F1FB65DE365C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c01376283e2e6f46e56214524f74a216f0d15d13","datavalue":{"value":{"entity-type":"item","numeric-id":2767085,"id":"Q2767085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f7a6111b9ee5cc25baa6cc4a337d2f10d730d17","datavalue":{"value":{"amount":"+0.7762971520423889","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":"Q4371519$ED64CD06-9E24-456D-ACF0-32D5FA3A1981","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d21618c33755d34119c83c7d442dd2530ec4786f","datavalue":{"value":{"entity-type":"item","numeric-id":4004176,"id":"Q4004176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"888357a7a78f59171fbac60ec5f659ff060d5792","datavalue":{"value":{"amount":"+0.7653009295463562","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":"Q4371519$0FB3D48E-913E-4C7E-B731-054F05F2FF58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb57dac5e9733bbbaad6a936013c102dabfd2939","datavalue":{"value":{"entity-type":"item","numeric-id":4419604,"id":"Q4419604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1ad0aad10f984b854fb74c41373f2e482180c43","datavalue":{"value":{"amount":"+0.7614123225212097","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":"Q4371519$173A31F8-479A-41C1-A1C3-9126D3F4C7C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0adab14be603a93bde827af0da3bc9888b83cc92","datavalue":{"value":{"entity-type":"item","numeric-id":4230664,"id":"Q4230664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c0d7e884f5552c51c28fab836a08941f8970925","datavalue":{"value":{"amount":"+0.7380906343460083","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":"Q4371519$C2343494-3315-4329-B277-64701E421529","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4371519","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4371519"}}}}}