{"entities":{"Q3003307":{"pageid":3014031,"ns":120,"title":"Item:Q3003307","lastrevid":58097055,"modified":"2026-04-03T19:13:32Z","type":"item","id":"Q3003307","labels":{"en":{"language":"en","value":"A focused sequent calculus framework for proof search in pure type systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5900060"}},"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":"Q3003307$3CB765E1-A37A-461C-89A7-6A08BD290878","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c73afd1c31700574c9fda62ecf1194fe58ff43f3","datavalue":{"value":{"text":"A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3003307$07036727-C9C1-461F-9CF6-DF60D187BA7B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a38bed6e84c6fa416ca03d29749cbca9dfcfc3a9","datavalue":{"value":"1218.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003307$39DB41DC-BCB4-4B5E-8C20-42E99C9F84E5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d50d7ed93ac635b29421f42a1dfe5aaa34b72d05","datavalue":{"value":"10.2168/LMCS-7(1:6)2011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003307$3ED1CC64-8A7C-4FBC-8EF8-47703F421078","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d79cf40c9d083fd33fffca7f5d652f193d57871","datavalue":{"value":{"entity-type":"item","numeric-id":876040,"id":"Q876040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003307$5137405C-6DAA-4EE1-BE64-F8BE3FFADDB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f07b5b97e9021286534ec61e4c6a7a24654de93","datavalue":{"value":{"entity-type":"item","numeric-id":452346,"id":"Q452346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003307$F241201B-B608-44B1-B898-7C05BB8E6731","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d6d72c052d6a5ad7a719f388761353f23640a4e3","datavalue":{"value":{"entity-type":"item","numeric-id":1725925,"id":"Q1725925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003307$86B2E625-B9BA-4AB2-BAFC-EBD9ACD241D1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003307$8C5EF299-EA4E-4B07-9228-843581CCB83D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d0d41ce3332fcf97fd23ad798d4a05a02b8284bd","datavalue":{"value":{"time":"+2011-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3003307$38B04F4B-39EF-488C-897B-E41AA032D49D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b99acc4e48f90d9aaf222874309414a02fc3846d","datavalue":{"value":"https://arxiv.org/abs/1012.3372","type":"string"},"datatype":"url"},"type":"statement","id":"Q3003307$C34AD081-A002-4278-A1C0-4E6FF415895C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003307$D00BEC96-6673-4429-B395-089039A7DECA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003307$38C64FE3-4A06-4AC1-B409-3EC3440EBD6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003307$21F19E43-5421-4EBC-8EB7-3B2FF751A1E7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"dd445e698ea0eff163294d64cf37dce81b17fdaa","datavalue":{"value":"5900060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003307$23CDAAB5-2855-46F0-97CC-39940FCB11F0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003307$8D94DFAF-0759-4479-968D-D1368FDA56F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01630645c8593048c51f927907064532b5b31748","datavalue":{"value":"PTS","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003307$B41D983A-0139-4BB2-83F5-CA0AD3BE2024","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003307$486061B0-DFE6-47FB-A0DE-E4D921C4D172","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d8bb84bd86abec9f57c8cf048201e810211b8ba","datavalue":{"value":"strong normalisation","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003307$0F16B181-6E03-48C1-A094-DE85196C22C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b8a9646b82dbeb50d8df2be83409261d3b2042d","datavalue":{"value":"proof-search","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003307$CA35502E-F1E4-46F8-AAB6-59A8B8E23C56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3fd3e9ac85afddfac937c2bfadba05c5617f051","datavalue":{"value":"metavariables","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003307$1BDA09F1-C31F-403D-9972-A8F8BB5A6BF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4ff1f8647fefa6ce5c1d1b9e7cde517a16fa5734","datavalue":{"value":"interactive proof construction","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003307$ED93D88E-7697-47F5-8D36-99B4F9010741","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003307$37381B63-1F6E-4E44-90A7-7C6DAA522FBA","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":"Q3003307$A440006B-0DC3-4DB8-8F74-3CF770CE8BBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003307$0CE117E9-CC26-42F8-8F21-9384CCF42F32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003307$5C7114CB-3BB6-4393-A97E-E00B3CA9F590","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":"Q3003307$0296B923-14BA-4E02-85E1-7AC530152182","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0cc095d956e2f62a7736c35b6868b8b7ee10cdf7","datavalue":{"value":{"entity-type":"item","numeric-id":3613355,"id":"Q3613355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9aded81c1b64fb55b620559cd0e220e01b1633e4","datavalue":{"value":{"amount":"+0.908263385295868","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":"Q3003307$A17806B6-6C61-4503-AC5A-D1A191BA286A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca32bfebc5ee8b344c13dade8a516a1005272067","datavalue":{"value":{"entity-type":"item","numeric-id":4924532,"id":"Q4924532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d02bb9353f066606054a060b2d9dd5e8e662f4e4","datavalue":{"value":{"amount":"+0.800452709197998","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":"Q3003307$862B2A48-1F8A-4937-BC93-3D36CFB0382D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"452b25f8262b4dc37f73326ee7da67099a47a43d","datavalue":{"value":{"entity-type":"item","numeric-id":4012884,"id":"Q4012884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51854ab8893a22e6d0da1653c132ab8c54c607f8","datavalue":{"value":{"amount":"+0.7824262976646423","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":"Q3003307$56ADD745-6885-4A55-8814-9D576DA91BAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1f536dd4897b55633cd8707e2d26ca95080188d","datavalue":{"value":{"entity-type":"item","numeric-id":5371956,"id":"Q5371956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51854ab8893a22e6d0da1653c132ab8c54c607f8","datavalue":{"value":{"amount":"+0.7824262976646423","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":"Q3003307$8A795D51-A6EA-41C8-BCEE-C55E38313EF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aaae8b02556144ce3ed7738674e0ec95ed9ff1f9","datavalue":{"value":{"entity-type":"item","numeric-id":4223032,"id":"Q4223032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4baedd7dc1ed12984180b8a5efa977a78fe3f735","datavalue":{"value":{"amount":"+0.7672554850578308","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":"Q3003307$7064D3C7-BF55-4F90-BD67-A3F528350315","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3003307","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3003307"}}}}}