{"entities":{"Q1373302":{"pageid":1384042,"ns":120,"title":"Item:Q1373302","lastrevid":67268058,"modified":"2026-04-12T16:29:18Z","type":"item","id":"Q1373302","labels":{"en":{"language":"en","value":"Abstract proof checking: An example motivated by an incompleteness theorem"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1089471"}},"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":"Q1373302$906DB08C-3B13-4B7A-ACFF-6B8501F28051","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0a5e204d790a7c42250ef1f12bedbcf6a0d348c3","datavalue":{"value":{"text":"Abstract proof checking: An example motivated by an incompleteness theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1373302$85F673D1-5238-4263-8287-3227DF87030E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5a98618bc59b7a9e4c984d1f23757309b9906c03","datavalue":{"value":"0890.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1373302$77A76139-4FB3-4134-BDE6-AA9BABA34885","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"104197d6d94af7b2f15c8174fa1ab64af540edd2","datavalue":{"value":"10.1023/A:1005877613942","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1373302$11B2E125-7C25-40B3-9CA2-F1309F7E6063","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d37a3d6bd9a0b44736f3bc6a6985f44383a95724","datavalue":{"value":{"entity-type":"item","numeric-id":438542,"id":"Q438542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1373302$B85DA7AF-B80A-494C-882D-37BEBC0E5BB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"99809ed495e654999be3f275423a0ba7027d3b10","datavalue":{"value":{"entity-type":"item","numeric-id":219437,"id":"Q219437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1373302$CA8C6A7E-08B5-4FB8-A869-0F98364E86B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c739d3ea0f609cefa3c6f88838b460e5722479af","datavalue":{"value":{"entity-type":"item","numeric-id":1373301,"id":"Q1373301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1373302$C47373FC-66AD-4599-9345-BEE3E54BA063","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f6a5cb47bfb987a892c1ea29852a7967462f77d1","datavalue":{"value":{"entity-type":"item","numeric-id":215106,"id":"Q215106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1373302$346E8625-FA25-484F-A7D9-A5370B34ABBB","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":"Q1373302$B5E387A1-1C84-4731-8EFA-2E0731A8902F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f680ab37822a66c306de184badf1c6b2f8f85485","datavalue":{"value":{"time":"+1998-06-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1373302$D1B0D02E-6E9F-4A20-9EAE-197C0191A22B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1373302$0CBAF911-C0E0-45FB-8336-0F2F8C9B07A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1373302$8F5949F5-3735-4A65-BFDC-16F5BD98DF2A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a70794d47ee8a11730e93d2a6befc32ac384744f","datavalue":{"value":"1089471","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1373302$AB373B73-5793-4064-A752-26069F050E8C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a614927b0caf638748bb51c0de92c1b49104311","datavalue":{"value":"proof checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1373302$72A4CD39-AE3E-4D1A-9120-C4662332FA38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e404e0d47002bfb1532cb42cfe324606a2151619","datavalue":{"value":"abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1373302$5374A8A7-541F-4BF1-BC6E-F682DC91CCA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b32bc21a81f9a57bf0c704682dd12bfe644d62d7","datavalue":{"value":"interactive proof checker GETFOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q1373302$CCB385A2-8875-488D-AFE4-9E0CE2C2E9C4","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":"Q1373302$E2008DFD-636F-44A1-8414-15BD77A708AC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"594f42eaca465cf3f11c2e90426f7d6d3921a19f","datavalue":{"value":"https://doi.org/10.1023/a:1005877613942","type":"string"},"datatype":"url"},"type":"statement","id":"Q1373302$B2CA1E83-FB1E-42AD-A041-87F48F3B4183","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a9f084c7490c1ed2a850140e70bbfec76fda2998","datavalue":{"value":"W1558960796","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1373302$C26346E1-1889-4675-9437-D88243E5FCC3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5153f4ee260d21542ec2b89d7787fd721bba360e","datavalue":{"value":{"entity-type":"item","numeric-id":3490995,"id":"Q3490995"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f16945d7059ddd5df9ecdd6b31cc561afbf92aaf","datavalue":{"value":{"amount":"+0.785748302936554","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":"Q1373302$E42DAC74-9415-4A92-A240-887A4FA54D64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a61a1fcb87b25a45cb977364794737a271e69d38","datavalue":{"value":{"entity-type":"item","numeric-id":5894725,"id":"Q5894725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f85c4c879dc85a695126c66916cc2b393e328bca","datavalue":{"value":{"amount":"+0.7251320481300354","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":"Q1373302$F655E08D-0F32-4C96-A0C3-E2D34BDD6C9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ef6f8cd8718f1d64bdad3d35d2a8750a28f6eb9","datavalue":{"value":{"entity-type":"item","numeric-id":3759967,"id":"Q3759967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b97b5b74b5171f4a84474b316388fe194bb557a","datavalue":{"value":{"amount":"+0.7231120467185974","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":"Q1373302$F5021F1F-DFBA-4CE5-BAEF-4C6963E73020","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1335255e53437e5ef4f817148c595db6c02a4ba8","datavalue":{"value":{"entity-type":"item","numeric-id":3024890,"id":"Q3024890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d36a8623f452c1295dd93f6a3244dc99c28495c","datavalue":{"value":{"amount":"+0.7207459807395935","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":"Q1373302$6075C26E-DC20-4F9D-903F-36D753A20DC2","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":"496c5984a4b8ac2dcf0022c07aace9aa21b407fb","datavalue":{"value":{"amount":"+0.7147800326347351","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":"Q1373302$F1FA4E9D-B1F4-4D6A-BEE2-AC52463EFACF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Abstract proof checking: An example motivated by an incompleteness theorem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Abstract_proof_checking:_An_example_motivated_by_an_incompleteness_theorem"}}}}}