{"entities":{"Q2946696":{"pageid":2957416,"ns":120,"title":"Item:Q2946696","lastrevid":85133678,"modified":"2026-06-03T06:00:31Z","type":"item","id":"Q2946696","labels":{"en":{"language":"en","value":"Instantiation schemes for nested theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6483199"}},"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":"Q2946696$B19E5D41-4271-4FE3-B092-01B57EA1708B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fa97069306316bd32dce666063ed7ac1545f2e97","datavalue":{"value":{"text":"Instantiation Schemes for Nested Theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2946696$306AB6FA-1675-4E5B-95E9-B2A53634A2EF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"59320b57b95d2a8e9c3c5cba58b4872ede140703","datavalue":{"value":"1353.68249","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946696$D180B9A4-094B-4CBE-8B37-BA003DA9DB9B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"206ead506f944d51b3c31e7da6e97d399635d77a","datavalue":{"value":"10.1145/2480759.2480763","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946696$B54C83E9-9C27-4E1C-95B2-990A7B4D29D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"da9d0bb1bba7f8d78f26f8b0456c3cbe905220ef","datavalue":{"value":{"entity-type":"item","numeric-id":438577,"id":"Q438577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946696$B5786FE2-6116-4F76-92B5-78BF5A421DA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dbb66b347a8501d3e88bb4fc6db185a6021261a5","datavalue":{"value":{"entity-type":"item","numeric-id":167063,"id":"Q167063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946696$9BEF8643-6EBA-4DC8-82CD-1F979ADBAC14","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ae5381e7211b64f5f54296c18dfaf60be613ba86","datavalue":{"value":{"entity-type":"item","numeric-id":2946565,"id":"Q2946565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2946696$6777F2AD-A468-424F-B984-50A4BB98D143","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ce093f9954be490f07dc8f1174896bb5ed4d11b0","datavalue":{"value":{"time":"+2015-09-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2946696$3B9A76F7-1324-4211-A416-24E5D1C67745","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6a53f22c95b4f60435bd0c556546313f96dc9dc3","datavalue":{"value":"https://arxiv.org/abs/1107.4937","type":"string"},"datatype":"url"},"type":"statement","id":"Q2946696$30117F9C-5F1E-4325-8C14-ED04E815F2D1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946696$BAEBF1EE-E459-422E-9A7A-45B1DC68E52E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946696$29E1724B-4605-4B39-BE47-2F70932B861A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946696$E6948C1D-2E2E-4DEA-833E-84B1CC6D8033","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e3e4f2e06f0bd9adaee6016f55dfaf92a50cbaa6","datavalue":{"value":"6483199","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946696$0E56CAC5-041B-4761-A69C-535F1EDE3719","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"38df12d14f3e19f8260855c2e4203e50d878e4e5","datavalue":{"value":"instantiation-based proof procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q2946696$5F2BFD54-CBDC-4CA8-BF3F-EE59248CC04F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bfff88c2380e4c25bc3fa0710ad2e9544dd0740e","datavalue":{"value":"combination of theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2946696$79F559A9-8C97-47F2-918A-6B3427100887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2946696$08699219-0B38-4F4F-8FE3-0D487C7E76E7","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":"Q2946696$B19D4265-8B39-4D73-A00E-34C134A630EA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"07ec8faac4c409bc627809c948a2dd41ea00b6cd","datavalue":{"value":"W2030508846","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2946696$6DF20158-D6F0-447A-9E6C-C92332258253","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5cde24298f23a5b7bc7c7603ce121b3af6925fa","datavalue":{"value":{"entity-type":"item","numeric-id":1944184,"id":"Q1944184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a12a6f1c3ec614d58edaee7cb0f7a51a62ea6aa9","datavalue":{"value":{"amount":"+0.8131057620048523","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":"Q2946696$73A5A38B-DAD7-4619-848D-D2746A3104CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44f5333c900d359772d6b5aecd422238f1cecf5c","datavalue":{"value":{"entity-type":"item","numeric-id":3533130,"id":"Q3533130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7e4559d2a4eb00a0af6609fb5d5e05263cfa97f","datavalue":{"value":{"amount":"+0.7473957538604736","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":"Q2946696$2C22AADE-8FC8-4C20-B00B-21E1F96EF257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a163d4150362be8e1e2f5d5bb6dfb8185f2a5266","datavalue":{"value":{"entity-type":"item","numeric-id":5387915,"id":"Q5387915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89693e33417f761b26a7343bde1133ccf953d99f","datavalue":{"value":{"amount":"+0.7417564392089844","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":"Q2946696$1641E490-C703-442D-ABCB-34F2D2987C50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e8af80161dc8c18c8bc8a8c02cd47c9c758f8f1","datavalue":{"value":{"entity-type":"item","numeric-id":438578,"id":"Q438578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e0b2541c6cee8210eecf19bb680402504f0cbdf","datavalue":{"value":{"amount":"+0.7295389175415039","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":"Q2946696$FA8C9A64-D974-47B4-85C0-F4F8753FBF6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"583cc387579d8b1388da91d5884e4a8bcd29c814","datavalue":{"value":{"entity-type":"item","numeric-id":1202066,"id":"Q1202066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33975502a16477b3aeabff0a8b0423c56baffda5","datavalue":{"value":{"amount":"+0.7229604125022888","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":"Q2946696$DCF924DB-52ED-43CD-9309-52A562DAF41D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Instantiation schemes for nested theories","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Instantiation_schemes_for_nested_theories"}}}}}