{"entities":{"Q2936769":{"pageid":2947489,"ns":120,"title":"Item:Q2936769","lastrevid":52166567,"modified":"2026-01-21T02:06:06Z","type":"item","id":"Q2936769","labels":{"en":{"language":"en","value":"Combining programming with theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6383914"}},"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":"Q2936769$2FE2C5EA-D0DF-4AA7-AB88-A33B943B6F7E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9e71940d96346fa7e1782560b919f48de6fd8d2f","datavalue":{"value":{"text":"Combining programming with theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2936769$0291CBE4-3CF5-4C9F-9783-9DF93C127417","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"94e240c2cd0ec185fc72e2d06fa82309d1854f4d","datavalue":{"value":"1302.68241","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936769$A860F99B-7980-409C-9D39-B1DA4E9DC675","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ac7c8bf539b6583d531521fde2d97f47291d4a27","datavalue":{"value":"10.1145/1086365.1086375","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936769$7F6FFCF4-FAD7-422E-A0EC-2B33C527D0D8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0b82d36e51997124a49664053ea8037a3ca5ffd0","datavalue":{"value":{"entity-type":"item","numeric-id":2936768,"id":"Q2936768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936769$71C79C72-2D24-468C-A096-2287FD6FA0F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bef15dcc9d238b439c915f4010ff60c2a860bd9f","datavalue":{"value":{"entity-type":"item","numeric-id":1286372,"id":"Q1286372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936769$0643D6CA-A829-417E-8621-61F3F12C62AC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"009f14fcff92f2b9864a3e960eefae33e15fd175","datavalue":{"value":{"entity-type":"item","numeric-id":2936758,"id":"Q2936758"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936769$F02AADED-830D-4C71-9DF4-DC951ADC3041","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"39d11daed231ddc9c09fdaf1d1bb16c5de77d47a","datavalue":{"value":{"time":"+2015-01-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2936769$F2426617-211D-4241-A989-313201DB23C8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936769$1C34E429-7B19-45E0-A3FC-391A3F3B49F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936769$1E2685A9-39C0-4C5F-9F28-6EE4270E34E5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"294fe4e660f1a224a9eecf1614cb7f5ed6e7fddb","datavalue":{"value":"6383914","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936769$6FEB19C3-F900-425D-8BD4-6DC1A6A6449F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"df796ad6812cb9a924f7cd549d9b0e5f8f83d61a","datavalue":{"value":"ATS","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936769$88CF64D4-28F1-4756-975C-2250E3CFF9DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aebc5a174ae42b1ed5d252dcd4e2ae1cc64c628b","datavalue":{"value":"applied type system","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936769$B3347E62-6726-4C98-92A9-F8DF566A9155","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936769$27A494BC-BDC1-465E-8A02-3C8DD7086097","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"64043a523df48bc1328d52f88bba37cb4d48ff06","datavalue":{"value":"proof erasure","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936769$9E193D88-0D01-4AE7-A613-F9330B4D317A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936769$66D72CDE-4E52-4BB2-BCE5-D9FBE65B4437","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":"Q2936769$D24DE254-F8A3-48C2-8268-DB4D88244EB3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f7ee6dcd10ffe2dc38c8335565a7d4869354a920","datavalue":{"value":"https://doi.org/10.1145/1086365.1086375","type":"string"},"datatype":"url"},"type":"statement","id":"Q2936769$3072A9B2-6E30-4D26-9F0C-1766EF62179E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"16fac63f46273340a24c9295037c978076529edd","datavalue":{"value":"W2134801812","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936769$020A1379-E9D8-4A5D-B938-AC7E4B00B1D2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d790df35eefe2e96f852fbd8027802e91f7f931a","datavalue":{"value":{"entity-type":"item","numeric-id":5491909,"id":"Q5491909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1747d2136cf5aff4648fad2209ad22ba3eb004f8","datavalue":{"value":{"amount":"+0.822263240814209","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":"Q2936769$CDDEB71E-67BD-442A-A9FA-6853D6D6CECD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"881379a3fa914a298d877b279ed01bf7e4e2ddbc","datavalue":{"value":{"entity-type":"item","numeric-id":3086789,"id":"Q3086789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6863ab9d8c0fdca612d2c3a796abe495f79f5ff","datavalue":{"value":{"amount":"+0.8181974291801453","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":"Q2936769$6ABCC896-AA33-43DE-A19A-0A2B7D690E0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6410b9474e4bc5f036d868efcfc1a70baa6c53c6","datavalue":{"value":{"entity-type":"item","numeric-id":5712319,"id":"Q5712319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b17706d6ceaa30dde9d57d718b3063281e79c1da","datavalue":{"value":{"amount":"+0.7446302175521851","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":"Q2936769$1581E31E-64CC-4460-AD07-4886E6F4DCE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"787bce44c26bfa68c4bdd6a337d32f1925d9a163","datavalue":{"value":{"entity-type":"item","numeric-id":3757915,"id":"Q3757915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"674352a1bc8b7933da3b9475b3316deed20fb02f","datavalue":{"value":{"amount":"+0.689038097858429","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":"Q2936769$034782A6-BDD9-425E-B9AF-DFAB1BFD0E47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c823eb76233e4855e66828e769991a47beaee71b","datavalue":{"value":{"entity-type":"item","numeric-id":1190474,"id":"Q1190474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"63e5a15fdf8dd751042e71b7b1bbaa92d37fa43f","datavalue":{"value":{"amount":"+0.6879659295082092","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":"Q2936769$D62A2A27-B6AD-4184-AED2-2EC954DA91C7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2936769","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2936769"}}}}}