{"entities":{"Q2219381":{"pageid":2230124,"ns":120,"title":"Item:Q2219381","lastrevid":57793371,"modified":"2026-04-02T13:36:20Z","type":"item","id":"Q2219381","labels":{"en":{"language":"en","value":"Metamath Zero: designing a theorem prover prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7298557"}},"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":"Q2219381$BAA3A05E-A149-4BA3-A252-708D6182BB79","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"912232a3eda0b425cec164964c5640027ec19a7c","datavalue":{"value":{"text":"Metamath Zero: designing a theorem prover prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2219381$0BEE4E33-31DC-4EBC-B3B1-A50A37ADF222","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"05828b410a81041365baa48c9af88784cef78e0a","datavalue":{"value":"1455.68243","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219381$C35DE8EF-04E0-4ACB-A2BD-8D7BDCAFF1BE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1d64b8f414ba204a4d3a40c793d5cefafaa6517d","datavalue":{"value":"10.1007/978-3-030-53518-6_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219381$857BCABB-D5D8-41CB-AAFB-D40B4F41A65F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc45e6b9322bed7360e4aac2a42f8c73614b44f3","datavalue":{"value":{"entity-type":"item","numeric-id":1787138,"id":"Q1787138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219381$68415656-1EDF-4256-8E40-A74A3C4EF917","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"233394734482eba32ed4ee15da745b1ac2b96149","datavalue":{"value":{"time":"+2021-01-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2219381$86F26A45-3817-4E7A-A5CA-43160A14FFA4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"98e6875b2ee0282a2389cc812b8e6ecf2896007e","datavalue":{"value":"https://arxiv.org/abs/1910.10703","type":"string"},"datatype":"url"},"type":"statement","id":"Q2219381$B0E975E6-2255-4D20-86A4-D478369E075E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219381$7BB3B7D8-FDB7-4A7B-BA24-0CF2281B4AEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219381$2122F1CA-BE02-4EFE-9559-978BF8797DB9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"14dd7af3d9bd047b9db52aee67670427f979c002","datavalue":{"value":"7298557","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219381$C999501F-0319-4FC0-BAA9-749DEBC5277A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8e2a306bd3f67e1f80b157e85cb5fdcb9ba4708b","datavalue":{"value":"Metamath Zero","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219381$919A8AAC-C955-440A-BC37-21CA5F0AF172","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219381$9A0A2074-61CB-4D59-A6C3-C11B2145119E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219381$1FBDE454-14F6-4EFE-BB79-213BC0108DF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219381$4F423558-11D7-4C62-BAF5-FAFE21701866","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0ee896cfb1ff087f610f0ba90e90efefd52ab1b","datavalue":{"value":"metamathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2219381$1240FE44-0BBD-4700-AFEA-D6F66B5E6C83","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219381$4C667690-8012-4762-B6AD-7B6ACE71FF35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219381$E4DCA3DF-CEE1-4BA2-826E-653E5FF443B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219381$73C30FFA-DD2E-413F-B79D-2DEF26EB23F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219381$41B85AC2-FA83-493D-80F4-148E4658C719","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"550541b08bcfd7113a03dc69a25fcd69cb35ddef","datavalue":{"value":{"entity-type":"item","numeric-id":25224,"id":"Q25224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219381$E5C5B874-656C-4871-AC8F-66186CEE72D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c9e521c77db45807815f297bb0abd1f031ff43b1","datavalue":{"value":{"entity-type":"item","numeric-id":39832,"id":"Q39832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219381$257B2C62-CA75-47CA-8908-C035D1A68DF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a7de3809e549ab622397ccc7caf8aa4227aa8390","datavalue":{"value":{"entity-type":"item","numeric-id":40151,"id":"Q40151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219381$AC0ED1BE-B6B6-4A1E-B66E-AF4E183D8240","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":"Q2219381$6298183B-90AE-43ED-9206-CF5BB7805199","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2d2aff057ab02df4da9360b82529e348137e2d58","datavalue":{"value":"W3042577812","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219381$456F278E-FD71-4347-BC19-D2DC2A08234D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b17a0214d51531a33f29c301b3359a976bc5385e","datavalue":{"value":{"entity-type":"item","numeric-id":3484381,"id":"Q3484381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13044735d986499fe58ccb831bdf17b087302cd5","datavalue":{"value":{"amount":"+0.8988658","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219381$05CCF364-7E87-43C6-AE4E-BD732E25DAD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"db58eb35fc2e4fc32aa7cdbe7a0664d3aefbe74a","datavalue":{"value":{"entity-type":"item","numeric-id":2844812,"id":"Q2844812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be69d282c6965d6d78e0299d6f462f1a91b5de2d","datavalue":{"value":{"amount":"+0.8677647","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219381$35A3CDD1-167F-4C73-9653-913B5679EAE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2830883c821c59e8ea357fc4abf509bdbccc9c9e","datavalue":{"value":{"entity-type":"item","numeric-id":1945919,"id":"Q1945919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88c7fcaf814baa3915df8524a94d9fae89aa59e4","datavalue":{"value":{"amount":"+0.8661934","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219381$AFABA915-3705-488A-A000-75FFD688306A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b360687fbb91abbd8b131ebd7a12117c200994da","datavalue":{"value":{"entity-type":"item","numeric-id":5505501,"id":"Q5505501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe7cc9df5dc8c8e894a3750e2c70baa8bd626387","datavalue":{"value":{"amount":"+0.86023545","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219381$614C006F-F202-45DD-88D9-8FAEAFF0BEA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc5435931d86571d4360d36b2e13206d8d9bf866","datavalue":{"value":{"entity-type":"item","numeric-id":3118384,"id":"Q3118384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac939f75916b888e4e279905850d0a44eeccf241","datavalue":{"value":{"amount":"+0.85892844","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219381$A0565693-4ED9-41F5-8EC2-1C3039C0E209","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d8229f7daafb1debae26fdffd7e93734038545a","datavalue":{"value":{"entity-type":"item","numeric-id":5210800,"id":"Q5210800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66914553dc836c6c58b0fa13bfede3b1c67e988f","datavalue":{"value":{"amount":"+0.8579795","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219381$36D91F22-0E35-4CF8-BFB9-0A1BFCBB1963","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f43a6a78ed9954347147234636751fa5d4fb034a","datavalue":{"value":{"entity-type":"item","numeric-id":5191110,"id":"Q5191110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"baa31e7148fc16bb19af17015209f25e9c1fe481","datavalue":{"value":{"amount":"+0.8529394","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219381$DB8FBEE8-5366-45C1-8946-CAF9B9C02703","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fee10d282ff2fc3fce33a7dab740b6dc62ff8b0d","datavalue":{"value":{"entity-type":"item","numeric-id":3631203,"id":"Q3631203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"504d2a159247734ad52d1c6e50c8402b2c462f56","datavalue":{"value":{"amount":"+0.84884346","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2219381$28ADC305-D236-4179-ACD1-7ADD3B2ECF12","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2219381","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2219381"}}}}}