{"entities":{"Q3308161":{"pageid":3318869,"ns":120,"title":"Item:Q3308161","lastrevid":80693669,"modified":"2026-05-06T16:47:14Z","type":"item","id":"Q3308161","labels":{"en":{"language":"en","value":"Overview on mechanized theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7235164"}},"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":"Q3308161$1404C4D2-6BC7-4E70-93DB-8166B0A27910","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0c6c9d6ad0ac2d96161f96671ca6caabb1db497a","datavalue":{"value":"1449.68143","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3308161$C47A3EC9-47B4-465B-A8DB-7B9A906AEA9A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"807e8e4baa68275fabd8a6dc4a9a939980bfcbbe","datavalue":{"value":{"entity-type":"item","numeric-id":314703,"id":"Q314703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3308161$974F0505-B973-4AE0-ADE4-D0272964C90A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"99894b1fbabea836ce518ec19fd090ad788f21b7","datavalue":{"value":{"entity-type":"item","numeric-id":2982136,"id":"Q2982136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3308161$8C29A469-9593-4AB3-A073-29747FE3E540","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"95a5e7bd453c3099e0d1981275bc09f7ca867c0d","datavalue":{"value":{"entity-type":"item","numeric-id":3308160,"id":"Q3308160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3308161$5364F3C5-39D2-47EE-83D4-7DB48D96E0B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"342142834e1074899b4783841e4d8f194729dea2","datavalue":{"value":{"entity-type":"item","numeric-id":991027,"id":"Q991027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3308161$2BAE42AD-1E39-4B02-A4DD-C1D2BD327EDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"07834aa8c7cc7db8ea5f70286994dc1fbe1a4261","datavalue":{"value":{"entity-type":"item","numeric-id":436740,"id":"Q436740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3308161$F9F7AB3B-8A8E-494D-B9BA-F918F7861E22","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9a0601910279d3cd6e6f45d9bc6255b7f45b2ef8","datavalue":{"value":{"time":"+2020-08-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3308161$01FAF8DF-43CE-4D17-8299-6C102E6A0C3C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3308161$71A6BD1B-B383-4EA3-BC06-0698DDD46E34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3308161$43E10E1C-3276-4CF2-926D-5747D355FAD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3308161$DB83C0A3-4E49-4F3C-BE27-068A19AA2384","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3308161$F4BC279A-CA92-4C3A-BFF4-2FF76CC228AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3308161$D1412A9D-B1EE-40DF-9078-056C0830534B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a8e0d5756af9ca0bb5710a9bf18d2a5b691e308f","datavalue":{"value":"7235164","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3308161$3E2233E2-CA12-4D25-A3AB-7302E7E8460F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3308161$FD66AFBA-D471-4792-91C0-34B02167B897","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q3308161$DF505FA3-BDCE-40F8-8EC3-CF7E71CB4DB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"96125518bbd73c679654439d2a0c9178b4d2695c","datavalue":{"value":"\\(\\lambda\\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q3308161$E7647884-CDC3-43C2-9838-0BFFAA802E75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7b8fabb834806b8eac85861850d6b5bc78f56e6d","datavalue":{"value":"logics of programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q3308161$DE8BD4D3-C1A2-4779-9AA8-708C4D24A3DF","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":"Q3308161$0B283841-7F1A-4EDB-ADF2-08B852295FE3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4b92566e40ed03c507d73010c830e0b9f8dfa616","datavalue":{"value":"10.13328/J.CNKI.JOS.005870","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3308161$2970464E-19F8-4295-901C-65695A4839BD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e95534a651efba3d65a2767b50c89b962d50b1d8","datavalue":{"value":{"entity-type":"item","numeric-id":3021914,"id":"Q3021914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d76a8371f2736ccd93565d6fa233180287e192a","datavalue":{"value":{"amount":"+0.8136098384857178","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":"Q3308161$0BB921EA-FE48-4D27-BE8E-2DC80F9FEFCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5caf9de33d1799cb19ca4a87514a35fe4bcf1918","datavalue":{"value":{"entity-type":"item","numeric-id":704001,"id":"Q704001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ae38e94b113ea124ccef30b490d9af1240ed0a0","datavalue":{"value":{"amount":"+0.8040627241134644","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":"Q3308161$F4560386-BCA0-4563-8092-E1D4258FFA4D","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":"4804a80a950e71e55e75a1342e4150d4ee965c1a","datavalue":{"value":{"amount":"+0.7721651792526245","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":"Q3308161$E4A71C87-D22A-4606-93CA-A834E0151803","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c464355e162bb39742d35675ae4f88b3e02fa0d","datavalue":{"value":{"entity-type":"item","numeric-id":4370791,"id":"Q4370791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e1f760219ca2845450ad352631b0126443cecc6","datavalue":{"value":{"amount":"+0.7694281339645386","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":"Q3308161$0826CA4F-8C8E-4452-9703-EDA50BCD37BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c8162a59b8a13ef31c7b2c2cfc782b60b654f3a3","datavalue":{"value":{"entity-type":"item","numeric-id":4503919,"id":"Q4503919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab6092207adb5092256edafcbbf65b94083cdb32","datavalue":{"value":{"amount":"+0.7664360404014587","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":"Q3308161$73F3D856-33E7-4979-B504-CBC853FAACF6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Overview on mechanized theorem proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Overview_on_mechanized_theorem_proving"}}}}}