{"entities":{"Q779163":{"pageid":781012,"ns":120,"title":"Item:Q779163","lastrevid":64316166,"modified":"2026-04-11T19:02:46Z","type":"item","id":"Q779163","labels":{"en":{"language":"en","value":"Proof search algorithm in pure logical framework"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7223680"}},"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":"Q779163$2838977D-AABC-4223-B602-A2F90188CCC6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0c38bb52a0815537de73e4eea1d38695936ab1fb","datavalue":{"value":{"text":"Proof search algorithm in pure logical framework","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q779163$472944BE-24D5-4F12-927E-3334E874C9A1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e2d9c9d2b8e6b35051f02bfef4562df8631b1ee6","datavalue":{"value":"1451.68327","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q779163$64A9B2B6-9FE3-41EF-9379-1F47925E5950","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d4d67d8df930b1130da626eccae828e4ebe1484","datavalue":{"value":{"entity-type":"item","numeric-id":779162,"id":"Q779162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$65D4862C-8984-43C4-BF7D-77FC13CF1F37","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e352e5fed1237b3989bd37f56da7d305fcb36e06","datavalue":{"value":{"time":"+2020-07-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q779163$6603BFE7-C555-4FA4-844D-4392E2ABD108","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"82435adf8d636d58ad223f1ae006a4a41bd480a6","datavalue":{"value":"https://arxiv.org/abs/1710.06181","type":"string"},"datatype":"url"},"type":"statement","id":"Q779163$87CB27BF-441B-4AE6-B5F6-1A32A26E81C7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q779163$968486D8-8CD4-4B4F-862C-E46800134E1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q779163$DD3036AF-D78E-4891-BB30-64E881AD4CB1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"594f892eae30d0d03c228a082f64aae5a9124eaf","datavalue":{"value":"7223680","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q779163$0E263F9A-F1A3-48A0-9A8A-7B11299FF36D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q779163$F9692BC1-DCCB-4D1A-B9EA-F46A0ED27434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95c030d9a0c4c312aef7a319ac8b5849913b2040","datavalue":{"value":"logical framework","type":"string"},"datatype":"string"},"type":"statement","id":"Q779163$D8C5BBC5-53C9-4483-992E-0F2005D0928F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bf9e1fc0dc8d08418a1a59ad167ac8072c4c07f6","datavalue":{"value":{"entity-type":"item","numeric-id":25226,"id":"Q25226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$76B690FD-3D99-438F-90F2-B9C1DA922E86","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":"Q779163$043EB5AA-F083-4233-A982-90BF579EA7E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$DCC4A17D-0FC5-4D3A-ACEB-74B5E22A5090","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":"Q779163$4BD27C48-5B31-45FE-A2E0-90DC88453D03","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a1cb03a574eec0cefb65dcf74ca9a2003a3256f9","datavalue":{"value":"W3117991794","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q779163$5B76F9EA-4A85-413F-851D-C187C165A227","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$2A4C568D-5674-4B65-A5F7-865784B1F81B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb87030458893ce6a5226c20f4768389b71ec39c","datavalue":{"value":{"entity-type":"item","numeric-id":2751362,"id":"Q2751362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$469A50AC-6E47-4171-9DF4-11E8C74A75E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f707d41b44671464c5d9fbd310386196c74d6c07","datavalue":{"value":{"entity-type":"item","numeric-id":2751378,"id":"Q2751378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$64620D80-EFBD-467F-B437-1A220E4DE295","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cb8e50e6c3bd60a9a9a59407cf30e8e788baa4","datavalue":{"value":{"entity-type":"item","numeric-id":3618853,"id":"Q3618853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$F3C6C87A-190E-4D3D-A62D-4FFE918C2652","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67f63602864ba0f92673863c4e08e8c412c43a5e","datavalue":{"value":{"entity-type":"item","numeric-id":5845381,"id":"Q5845381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$6A602097-EE12-4683-8FEA-4F0B32BC887C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1f3e0d3ccdd5ec8618c022752f1b192d7395e28","datavalue":{"value":{"entity-type":"item","numeric-id":5614670,"id":"Q5614670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$12DC268E-41BA-4FD0-9ACF-15BDC36E4F64","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ea2b4cb57e79a26c06abda48ae7f003ddd0c3abe","datavalue":{"value":"10.33048/SEMI.2020.17.073","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q779163$F5438BEE-5C26-4F66-8FC2-47E60577D370","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b799d93c9c23571e42d1b0fdc710b5b584588fc5","datavalue":{"value":{"entity-type":"item","numeric-id":5224174,"id":"Q5224174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q779163$0E82D299-EB11-4CF1-8B44-4E0DB7C96426","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b97ad471e6172b61acd1f2b10b8e40a3cfe9a5bc","datavalue":{"value":{"entity-type":"item","numeric-id":3003307,"id":"Q3003307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccf513c7b7ceaf7dcb9850f1f3d6ca1e8cc6c846","datavalue":{"value":{"amount":"+0.7387312650680542","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":"Q779163$5B03824B-EE4D-4D0D-A779-AA961BAE5B1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a64c47bdc30203f90f4e8f7ff55f9739dfb7112","datavalue":{"value":{"entity-type":"item","numeric-id":3183521,"id":"Q3183521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c9cd4c4b954d6184b1d0eeb92597d367b5b6e38","datavalue":{"value":{"amount":"+0.7206818461418152","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":"Q779163$0CC899A6-14F3-4169-A13A-B25D2E0D4764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3360a61977a1ee968db1e29c50105216b7d324b3","datavalue":{"value":{"entity-type":"item","numeric-id":4268421,"id":"Q4268421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29a781fd7780926dac1da121f9e2cb6910310f06","datavalue":{"value":{"amount":"+0.7127187252044678","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":"Q779163$99F20F42-3F4D-404F-A242-46A02B2D12A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"523ceda9c46f837435b012e3131d159e916a802b","datavalue":{"value":{"entity-type":"item","numeric-id":1575928,"id":"Q1575928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47055b46469ad801f6cb756aae2af9ac89e7384e","datavalue":{"value":{"amount":"+0.7126901745796204","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":"Q779163$81892459-AC80-46D4-B70B-3DFF33047BE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"89e0aa4de4e6435497f61a9d892d2b27d9babdc0","datavalue":{"value":{"entity-type":"item","numeric-id":5415611,"id":"Q5415611"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46e173098c1113ea6e69bd46efc2987638f4e677","datavalue":{"value":{"amount":"+0.7116479873657227","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":"Q779163$8C724DFE-C89D-4592-B509-FEFB37ABCC7E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof search algorithm in pure logical framework","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_search_algorithm_in_pure_logical_framework"}}}}}