{"entities":{"Q1821563":{"pageid":1832305,"ns":120,"title":"Item:Q1821563","lastrevid":49053580,"modified":"2026-01-06T12:59:09Z","type":"item","id":"Q1821563","labels":{"en":{"language":"en","value":"Towards mechanical metamathematics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3999322"}},"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":"Q1821563$8492C03C-0553-465E-A2DE-72F7F355AB66","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"46e41b8586a6070435537ec6b9895eab97692c70","datavalue":{"value":{"text":"Towards mechanical metamathematics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1821563$EE7C4D08-7C5B-4154-84D4-D903E1AE657A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b8848b8fe270798233099f43ff479afc35120a80","datavalue":{"value":"0616.68075","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1821563$2856F348-2689-4A34-AB96-8992F32905EB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"aef7243db4cd1f97cd9c9ec8677207a18fb08eba","datavalue":{"value":"10.1007/BF00244278","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1821563$EB5B1F2F-F44E-4109-987D-EA040730A49C","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":"Q1821563$A91E3D91-103A-4601-82ED-5C151BEB9B03","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1821563$562438F1-94F6-4D2F-9F83-7141F32733F0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3c94df5c9af0ede578c52141befd29044de13172","datavalue":{"value":{"time":"+1985-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1821563$9C0E9A0C-6A5F-40C1-8ECF-D22B9AA66315","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"777d6201bdfed09481d6cf0b422c081a280b4c2c","datavalue":{"value":"Metamathematics is a source of many ineresting theorems and difficult proofs. This paper reports the results of an experiment to use the Boyer- Moore theorem prover to proof-check theorems that the prover was able to prove about this logic. These include the tautology theorem which states that every tautology has a proof. Such proofs can be used to add new proof procedures to a proof-checking program in a sound and efficient manner.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1821563$0EF04B39-C272-4F58-9100-E7CB0F36700E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1821563$DE70824D-F313-4867-8899-3C41956803D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1821563$29FF4700-C6CE-4304-842E-9942A4780759","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ad471e845a071af5b2d762277058066a16acb703","datavalue":{"value":"3999322","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1821563$9D60ECDA-13B9-49CC-9C4C-D4FD512FDA75","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06aca432496264a4189a9a8b528e128b9e01a6fd","datavalue":{"value":"mathematical logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1821563$1DB8D0C3-ABFD-4083-83B3-250EE103226B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d2aa687cef17cd912aad76972cec097c0540be8","datavalue":{"value":"automatic theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1821563$1095AEE0-C72C-4A53-B651-3D4E2DC269A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4c0499f825f10e97efcf90d90181fdf392b1a6f","datavalue":{"value":"tautology theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1821563$CE5EB2F1-D166-4F84-9BD0-BB9318699A1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb7ab1d8b23719dd6fb8c99dae02604890e68f85","datavalue":{"value":"Metamathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1821563$DD479003-04AA-4E3D-B83C-C5FCCFC5134E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"67935c9745e86097c5a009e8bb47d5846729f37a","datavalue":{"value":"Boyer-Moore theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q1821563$CED00DEF-477F-4AB4-B12C-9C401EA5BA2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b4db4b238cd272f27cc2a06ec9e3657ef8e0582","datavalue":{"value":"proof-checking program","type":"string"},"datatype":"string"},"type":"statement","id":"Q1821563$10184F9F-3E1C-4A27-BFC6-506AEB0E25D9","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":"Q1821563$751C71C8-F9C5-4963-8E0C-93C3A7F86409","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d2d156d27ba4ac79a032d9500aa1accdc2c7720","datavalue":{"value":{"entity-type":"item","numeric-id":4296962,"id":"Q4296962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bc8836d3b146b211c9921aa8c8998428030e443","datavalue":{"value":{"amount":"+0.7998213768005371","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":"Q1821563$D65DCE4B-D629-4DC7-AFC1-261BF0E2ACEC","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":"59205793e55644dc0070a5ab7dba51f3bd027e89","datavalue":{"value":{"amount":"+0.7972966432571411","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":"Q1821563$CC83419B-57B3-4351-9D04-1D25933C34C6","rank":"normal"},{"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":"ef863e981aaec4a10167626a68f3c045fc093fe4","datavalue":{"value":{"amount":"+0.7971763610839844","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":"Q1821563$E1E70049-402A-45F6-85B2-5C517ED91FEC","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":"5d8528f1b43fcd28d498bae6f8ae1cc78d76aee6","datavalue":{"value":{"amount":"+0.7702184915542603","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":"Q1821563$A70181C5-21A5-4700-8D00-D3F0D7C95ADD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97b6c84a206840a1fdaf076f6a3452df9c6fce3b","datavalue":{"value":{"entity-type":"item","numeric-id":3801105,"id":"Q3801105"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"504edb126787d9a0afc256455b4d2f4381558ea6","datavalue":{"value":{"amount":"+0.7679814100265503","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":"Q1821563$5DAA0EE2-F816-4B08-9066-CF53E8565F9F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1821563","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1821563"}}}}}