{"entities":{"Q4647506":{"pageid":6677087,"ns":120,"title":"Item:Q4647506","lastrevid":36461855,"modified":"2024-07-17T19:48:24Z","type":"item","id":"Q4647506","labels":{"en":{"language":"en","value":"ABSFOL: A proof checker with abstraction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001899"}},"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":"Q4647506$3A37DE53-DFFA-484C-8C22-A715A3E77443","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7d8ed5af34916634ae566e627c66276e38f0a7a6","datavalue":{"value":{"text":"ABSFOL: A proof checker with abstraction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647506$69F9BC82-3F3E-49DC-BE30-33EF9F2F6189","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"865e623114b9bab1be5e4a7380c6c2fcc0a3ef9f","datavalue":{"value":"1412.68226","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647506$2491D481-EBAB-44BF-A100-0AD8FF5FF078","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"906543825c5d96f57538b377c6079ed7c1e67f0e","datavalue":{"value":"10.1007/3-540-61511-3_74","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647506$959CAE84-7BA4-40F7-9125-D99943E16A93","rank":"normal"}],"P16":[{"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":"Q4647506$089D0DA9-47C6-4EBB-A3F2-3B041CC92088","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":"Q4647506$4F881CB0-DDBD-4887-B858-5CF90F0B553E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647506$D03B1970-7A5A-45B2-8AD7-A83425CA1711","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647506$27E8DE8E-FF6D-49CB-8E87-EBBE58A47DDA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647506$64EC7808-2FAD-4591-9906-5D2C8D56C341","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0c8c774b94ee879a79aa4d0788ee5e8ebd9af3c9","datavalue":{"value":"7001899","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647506$A37BAFD3-CC7A-4CE5-B7B0-D72685E1D285","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93cbbe3aacb0282d348cb5e7d78e394a1a6097ce","datavalue":{"value":"inference rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647506$47039A96-B6AF-4578-B719-C17BD737B0A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4b4eafe9b1cc937116b91ec36ac55daabda12dc1","datavalue":{"value":"current context","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647506$A9091DED-7F4A-444C-9A20-8B6453D1BEA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647506$9CDF61C2-7192-448D-AD91-394C43E3E130","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26ed17f0fa3b284d6eda2a0b6f59f94f851c6b48","datavalue":{"value":"elimination rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647506$4F992031-84B1-43E9-AA12-8EC38EA61ABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7fbe37157212b9464d1b5aad5ab2d49f6eb9144a","datavalue":{"value":"abstract proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647506$DFAE7B8B-2014-433F-87AE-307A1B636D45","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25ad95c9ef24ef7056a03fa9237878c8c0fa2aa9","datavalue":{"value":{"entity-type":"item","numeric-id":38038,"id":"Q38038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647506$0D9B3F24-02B1-49DC-8BA8-E5BF5096C34B","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":"Q4647506$92212884-FBDE-4666-A98E-F59AD3BB03A6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2cd27ba6fc68768e9108058797e49bf2a9ea0e7b","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_74","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647506$015B21EF-42D4-4762-A02E-A88C626B2034","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"975615846c358fa6efa02cedec198d25bbffb601","datavalue":{"value":"W1513879706","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647506$86A19A8C-2E87-4210-8172-44E2F532585F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3797ca9c060a8f45bbe361e29094c28dc7f292e2","datavalue":{"value":{"entity-type":"item","numeric-id":1199923,"id":"Q1199923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647506$FB7BF64D-0FDB-4221-A05E-BC0AC0A2BD80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39d1d8fb42339a481de309d10a4b5b6fb7e49eec","datavalue":{"value":{"entity-type":"item","numeric-id":1140436,"id":"Q1140436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647506$4D43AC6F-CEE3-41CE-8551-832377BE1E7B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647506","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647506"}}}}}