{"entities":{"Q2708306":{"pageid":2719045,"ns":120,"title":"Item:Q2708306","lastrevid":82799933,"modified":"2026-05-06T22:06:47Z","type":"item","id":"Q2708306","labels":{"en":{"language":"en","value":"How to avoid the formal verification of a theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1588163"}},"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":"Q2708306$A52E9E47-D135-4A5C-9B81-AAE373850E51","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"615e488fa7dcf32b004f844d551da158d694bd5d","datavalue":{"value":{"text":"How to avoid the formal verification of a theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2708306$BB6A7081-64B0-4E2B-A5A9-B3B50545B489","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"95c74a679d946d679f3a225a1933d0419f56912b","datavalue":{"value":"0970.68158","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708306$0661E67C-158A-4A59-A73A-8F15A71472F4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d9f71358bbdbd87e15f90c45b21f9769883d0dbe","datavalue":{"value":{"entity-type":"item","numeric-id":506822,"id":"Q506822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2708306$52881011-8CBB-42FE-8C25-4E0FA5B8A714","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7535d8318d2cc237543992cf7aa2bc918ea6c44b","datavalue":{"value":{"entity-type":"item","numeric-id":590180,"id":"Q590180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2708306$877C5138-799E-4879-B9BB-796311BC7AF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b1c3fa95c1005d09eff8ff2b881875054b11a800","datavalue":{"value":{"entity-type":"item","numeric-id":583193,"id":"Q583193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2708306$5969E917-D1A9-4552-8ED3-8097D3000F7D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b6c0c12789b1c65edf998b307fadc1a05e2a1e26","datavalue":{"value":{"time":"+2001-04-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2708306$9B5A6A72-9652-4577-B134-37DA9693D103","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3a2a71da026b00838694e6b509bf350bbea49677","datavalue":{"value":"https://semanticscholar.org/paper/11cf51412aaa6745fb7869e37c22fd308f841e33","type":"string"},"datatype":"url"},"type":"statement","id":"Q2708306$63CB05DD-B9C0-4945-8E38-D8A710E09503","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708306$A288C440-B06F-405F-B63F-C74B3026D251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708306$1FB4F76C-CDDF-4A3B-81B0-8F2B1C715FE3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"53d722f5035dce474b14bc9cbd75f95079846528","datavalue":{"value":"1588163","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708306$3F2C7F57-1C16-4D30-9083-8B24C8F2CA7F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708306$FBC54E69-2790-44C4-8DE2-96252BC558A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51f2a8941e17fdea2aa5adfe2baef7f0d6097c89","datavalue":{"value":"tableau-based theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708306$778029D3-75B5-4E74-92E4-4260D900B6F0","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":"Q2708306$C267B75B-A03B-447B-A975-11C22355A287","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a46eb57443612cd0400e288641c7f88e70035464","datavalue":{"value":"W2094976963","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708306$9F25AE5E-0F88-4145-B267-C94E860FA640","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8bb92584fe72ada7fac90965d98981dcf8a60fd5","datavalue":{"value":"10.1093/JIGPAL/9.1.1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708306$A25CDA68-4D1E-4821-8DDF-B9B72AA69049","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2322a21df36f02b2b9c16a6174c764d5fc949009","datavalue":{"value":{"entity-type":"item","numeric-id":3061274,"id":"Q3061274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2708306$5B384F1D-A58D-425B-A1BA-E8028C96443B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9fa222bbbc2ab4bdf7afb3ef0c4c8b8b7f68ce28","datavalue":{"value":{"entity-type":"item","numeric-id":5086225,"id":"Q5086225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f5b54ea79b5d48cbce19ead13bb3296052fdf50","datavalue":{"value":{"amount":"+0.7074779868125916","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":"Q2708306$B8BBC863-4463-4E21-A58E-95B4BDA5F1DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2565d9e77d9b51b905daa5bfbb63ce859f62d93b","datavalue":{"value":{"entity-type":"item","numeric-id":3345811,"id":"Q3345811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9943f181297458ded05de598b7c3e8ecf88d9b3","datavalue":{"value":{"amount":"+0.7061699032783508","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":"Q2708306$4514B699-319C-40D6-A5EB-CCCCB6E06660","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae1b97a6f9d5931d17692b9da0d3db3bb3213cf3","datavalue":{"value":{"entity-type":"item","numeric-id":3455771,"id":"Q3455771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"539eac67d7f9c4a1d72a6d533aa4631a9683e169","datavalue":{"value":{"amount":"+0.6993220448493958","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":"Q2708306$89752CDD-828D-45C6-AA85-7770FB4D480C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27834f8881d79d504650b55693f4830b894523f6","datavalue":{"value":{"entity-type":"item","numeric-id":4530805,"id":"Q4530805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78d1243b043339e6b72651935b730b895e936e69","datavalue":{"value":{"amount":"+0.6979960203170776","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":"Q2708306$F979632B-D84F-4315-A439-719E5872CDB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0474bbb2119d7f935ca56ebb01dcab6b168475b7","datavalue":{"value":{"entity-type":"item","numeric-id":4928436,"id":"Q4928436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6f02aab9f1de2249578baede3b7fb9f5111b470","datavalue":{"value":{"amount":"+0.6948320269584656","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":"Q2708306$FA8B63AC-149B-4CAA-ACBE-D266F778764C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"How to avoid the formal verification of a theorem prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/How_to_avoid_the_formal_verification_of_a_theorem_prover"}}}}}