{"entities":{"Q2871873":{"pageid":2882593,"ns":120,"title":"Item:Q2871873","lastrevid":79530176,"modified":"2026-05-06T14:07:48Z","type":"item","id":"Q2871873","labels":{"en":{"language":"en","value":"Higher-order proof construction based on first-order narrowing"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6244447"}},"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":"Q2871873$905EF08E-D92B-42C5-B827-336E3DF9281C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9bfd622398baa3a52aba82e4e83048499226a524","datavalue":{"value":"1278.03059","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871873$5695F2E3-A85F-46A6-B199-C296A9A41B04","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9a8c72bd141d161cc2a0cd916655acbe79456646","datavalue":{"value":{"entity-type":"item","numeric-id":2871872,"id":"Q2871872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871873$D507E9DF-7B8C-42CA-804F-FA86C586A6F3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c704b287c68a3d4d8361a025642d6eba13574eb","datavalue":{"value":{"time":"+2014-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2871873$C6D0B587-629D-4489-AE0B-EA6E1053686A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"be7acb31fa888eb199ebf3b79e0858da15033ec4","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S1571066108000388?np=y","type":"string"},"datatype":"url"},"type":"statement","id":"Q2871873$45843033-A0D1-4B1F-9D8A-BB5A4D195BB2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871873$FBD0A622-1088-49A6-8E89-996628E95543","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871873$96A0E3AB-A577-4359-ADA2-7494C6921D8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871873$3E265C34-11E8-4CDD-9D27-AFECDE9570BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871873$2BF67A6C-B558-4A8F-B907-297C54C0D049","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871873$7B75B1B6-4410-402C-B962-0BEE0A35C97F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"30a0e7f2f4db9d5e215fe498bda4c83a1adfda06","datavalue":{"value":"6244447","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871873$759E789E-4D2A-44A8-BE13-F5B14E03B58C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9c3fe1355cee26fa277b80b006823226e0c31aa","datavalue":{"value":"higher-order proof construction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871873$599CE0E3-9167-443B-8D27-878F79E24640","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50e20429622ec08ba47dc9e7a4c57de8bf8a42d9","datavalue":{"value":"narrowing","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871873$D0F7C5B6-1555-40FA-A60D-090D8E09BDD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66040eec798fa7d182443c16b59531175d83cf5e","datavalue":{"value":"logical frameworks","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871873$A21D5D6F-E7ED-416B-93B8-E9DB71DC167D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871873$37F6F47A-CCE4-4331-B55B-7C7AE000A16B","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":"Q2871873$40780E0F-FAFE-4D6D-8DE6-F0848B6D8D78","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7d5fe7a501983d8e5b4015b7f89537c716a45995","datavalue":{"value":{"text":"Higher-order proof construction based on first-order narrowing","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2871873$FC89B434-E754-48BB-9FB8-305D5E64F1AA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be161ec7f3b9536e6e38479daa2455b405ae4f3f","datavalue":{"value":{"entity-type":"item","numeric-id":4916079,"id":"Q4916079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f392527d70126219c82ef99a97d534d95bf272a","datavalue":{"value":{"amount":"+0.7599804401397705","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":"Q2871873$7A0B2FB7-1649-4EC4-8AFC-93285B1CFEE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"199875f95486d52f14e754299d49b27352bfc74d","datavalue":{"value":{"entity-type":"item","numeric-id":5428267,"id":"Q5428267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7cee5e97cb50a2d348f8c6cf2484f49fa4addd74","datavalue":{"value":{"amount":"+0.7230120301246643","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":"Q2871873$F4DAB4CB-73A9-47B9-A580-DF062ECF669B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9a78c41bc3cc611cf5c6ea68d56b3e56736cc44","datavalue":{"value":{"entity-type":"item","numeric-id":4028349,"id":"Q4028349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bc8586432d3fe94064192b381fd94a4e512e19ec","datavalue":{"value":{"amount":"+0.7171340584754944","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":"Q2871873$714990E4-F0AB-44A5-87BD-EE47F3B4A039","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d515466375177240c9a5a9d2e20b70905c14b4a","datavalue":{"value":{"entity-type":"item","numeric-id":5376325,"id":"Q5376325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8cb7df928335b41b214ac2044e2f30f7dfcc2b03","datavalue":{"value":{"amount":"+0.7148527503013611","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":"Q2871873$11802F12-3705-4779-9C22-399D566A5232","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83ead96eb0dad59b33308a29c10c00c5949abf9c","datavalue":{"value":{"entity-type":"item","numeric-id":2723415,"id":"Q2723415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e8fbd027cda2d50532a14c5e7389fbf728b3c3c","datavalue":{"value":{"amount":"+0.7135694622993469","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":"Q2871873$8B42574F-C2E1-41FE-80C1-AF3FF1FB5DCD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Higher-order proof construction based on first-order narrowing","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Higher-order_proof_construction_based_on_first-order_narrowing"}}}}}