{"entities":{"Q6091296":{"pageid":13225603,"ns":120,"title":"Item:Q6091296","lastrevid":56840991,"modified":"2026-03-23T18:20:48Z","type":"item","id":"Q6091296","labels":{"en":{"language":"en","value":"Meta-F\\textsuperscript{\\(\\star\\)}: proof automation with SMT, tactics, and metaprograms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7770421"}},"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":"Q6091296$C8224E10-7761-4493-A78C-7DF241910353","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cee1fb825b94ca10af17f549e0cdd147cf6b5abf","datavalue":{"value":{"text":"Meta-F\\textsuperscript{\\(\\star\\)}: proof automation with SMT, tactics, and metaprograms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6091296$68CD21CB-3AD7-4F91-B27E-A91FC29DCD17","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"04ff57bf200490ccd430792f73c005973acc8371","datavalue":{"value":"1524.68195","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6091296$2B0966A1-A8EB-4907-AB5B-F643FA48E5EB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8fa02c684a27eecbf0b127c34781fc7b90c4e956","datavalue":{"value":"10.1007/978-3-030-17184-1_2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6091296$2468BCEE-1EDE-4265-BEE6-4CDD02D2B5B7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4b7b6d941015a5fa0f2f56a7af173d22723b85a3","datavalue":{"value":{"entity-type":"item","numeric-id":2333317,"id":"Q2333317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$FD375FDF-0BE0-4B8E-915C-CF0162F2B810","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6dcd7850e46a0b0acd4be366ca173c3191291ad8","datavalue":{"value":{"entity-type":"item","numeric-id":265790,"id":"Q265790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$6CDC87D7-8901-41A3-9D2E-68210583C71B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"069cf24700f5fa5a91d8f59359d7d11fb63019ab","datavalue":{"value":{"entity-type":"item","numeric-id":6091294,"id":"Q6091294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$4E6FDEE8-5F23-43BC-A3DE-6985D2ED214C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0dc8882bc452ee46479207f2875e5460c0df055c","datavalue":{"value":{"entity-type":"item","numeric-id":2828303,"id":"Q2828303"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$FEE8F0EE-939B-42A7-B1B1-45CFD4887604","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0cbe4fb87bde48f3abef1fb879b8863c4192a481","datavalue":{"value":{"entity-type":"item","numeric-id":1852266,"id":"Q1852266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$27B6BB05-09A8-45AA-9ADD-FD8BD9F32F59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9dca520b2b44c51b0ffb92f2dd255590e5e0e273","datavalue":{"value":{"entity-type":"item","numeric-id":2324195,"id":"Q2324195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$A51BA4D3-59A4-4321-B711-9091BCA2B362","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6870638c46b4037547ad92b21b468c973ad162c6","datavalue":{"value":{"entity-type":"item","numeric-id":6091295,"id":"Q6091295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$2B36EB9E-8ECD-430D-92CE-863E474C3F18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f58bf2e7115000c32a013ce9908b790af2d8edcf","datavalue":{"value":{"entity-type":"item","numeric-id":2945643,"id":"Q2945643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$4EC40F33-9733-4592-8EAB-29D6CB3FAB57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ebd22af850026676982d2d243b86cdd14bc9a72a","datavalue":{"value":{"entity-type":"item","numeric-id":2819860,"id":"Q2819860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$BE620C79-BA36-4E5E-9600-C11411FAA02E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6aa6df7e2a86cf1469554b56a008ebabd8ceb658","datavalue":{"value":{"entity-type":"item","numeric-id":5170716,"id":"Q5170716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$FB0D1BC6-5264-4A23-889B-7E3AD83E58ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c2f7c005f4bee573bde0aed29ab3973980cc4fa","datavalue":{"value":{"entity-type":"item","numeric-id":2819846,"id":"Q2819846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$DF0D180E-83F3-4C0F-B727-AA8E42646F17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4efe461cd9841e8acab75aaa516869b7bed4e3e1","datavalue":{"value":{"entity-type":"item","numeric-id":2819799,"id":"Q2819799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$C65C7367-50D1-4523-B335-7E715E17C9B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a9c43047206e58c5aa24afe8babee124065c6b77","datavalue":{"value":{"entity-type":"item","numeric-id":2819800,"id":"Q2819800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$A6D47375-6EF4-4A3C-ADC0-7EC7C1D7AB91","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7efb66db9d8cc237b51d0f645d1a54c929d4c460","datavalue":{"value":{"entity-type":"item","numeric-id":2789030,"id":"Q2789030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$95F516F7-72E9-4433-B800-3ECF56DA59C7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"23cd7302534ebac1f5798f1388e7a545a7b25124","datavalue":{"value":{"time":"+2023-11-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6091296$071CBD8E-D1C8-4F07-972F-4A5817696348","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6091296$BD6A4032-D9F1-433B-952F-2B9F48D85964","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6091296$DAF23560-30BF-4385-A266-7E4C5F936E72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6091296$8B90EFB4-AA3B-45F9-993A-6600A0CE8462","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"16ec3b7883ee2d83847be43c03bee3e7b9f10bf3","datavalue":{"value":"7770421","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6091296$59AFA908-73D7-4C94-83EC-07766FD497AA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c80ecf21428f980362763aa3ec34b156b15c6fc","datavalue":{"value":"tactics","type":"string"},"datatype":"string"},"type":"statement","id":"Q6091296$A102754E-9B58-426C-9006-525151DD4993","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"329d09641862ba8331cecdfb9962e139d99ecf56","datavalue":{"value":"metaprogramming","type":"string"},"datatype":"string"},"type":"statement","id":"Q6091296$40282BE5-F4A4-44AB-B707-29D00D288F74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6091296$4F4A215C-E27E-459B-900A-A56082B9AD32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c466a31828be4527e6fa92732efebe73d5786789","datavalue":{"value":"verification conditions","type":"string"},"datatype":"string"},"type":"statement","id":"Q6091296$E14969A4-C166-4BCF-8389-A7C49F52E938","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61439d791f6aac729372268f16b553bcf47e3b78","datavalue":{"value":"SMT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q6091296$006EA7B4-B607-4223-AC0C-8FBD517AF0D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q6091296$76CAA7B9-196D-41CC-A023-C22ED11957B4","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":"Q6091296$E6656696-BE24-4A47-907D-11C68C3B7AEB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3394927f38671d05b1b976613e176ee96a3ccd44","datavalue":{"value":"https://doi.org/10.1007/978-3-030-17184-1_2","type":"string"},"datatype":"url"},"type":"statement","id":"Q6091296$FEF7CF5E-BFD4-4EF3-B3A8-65990BEA8255","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a741738009f62d0beec18761376628d6c19178b1","datavalue":{"value":"W2839528116","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6091296$EC11A48E-4F9E-4862-872A-2B2430983C8F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87d8460ce4f486383b05ac93c44ee0afdba81933","datavalue":{"value":{"entity-type":"item","numeric-id":1791152,"id":"Q1791152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98daa466f736521760a3e0cc25721673a7e1bd6b","datavalue":{"value":{"amount":"+0.7760144472122192","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":"Q6091296$9F97C2EF-35E6-4839-AA5E-77A38B5C719A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c8fc519c81890f963ff41e9abebedea516f59fd","datavalue":{"value":{"entity-type":"item","numeric-id":5371944,"id":"Q5371944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a02996a428c87049acaec69a7b1e469360602e95","datavalue":{"value":{"amount":"+0.770054280757904","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":"Q6091296$B555F888-ABA8-4BD0-A12D-467F808B3E28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3e572badf5bee00e7427a40b4cef297ea325698","datavalue":{"value":{"entity-type":"item","numeric-id":5244791,"id":"Q5244791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84618683f29aabb231f2e567710d4f436cc5a94d","datavalue":{"value":{"amount":"+0.764045238494873","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":"Q6091296$2C5C175F-84F8-4236-A842-571FCA6FD2E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"435c230f2e936567467c911556c7b07e730f6c8f","datavalue":{"value":{"entity-type":"item","numeric-id":2802496,"id":"Q2802496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d392222e7fb1447dd29cd7f999f4075cd25e5ff","datavalue":{"value":{"amount":"+0.746246337890625","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":"Q6091296$769DEB9D-5613-403D-9974-7200ED192489","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"91b07f7752f048810838a13b3751f9f4416cde07","datavalue":{"value":{"entity-type":"item","numeric-id":2828265,"id":"Q2828265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"881c110075aa5121364a2b496054db8763f8b6e1","datavalue":{"value":{"amount":"+0.7436404824256897","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":"Q6091296$3861E38E-895C-4624-A073-B5AEE53381FC","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6091296$DDAB1314-918A-4874-8C2A-47AC9DA80F89","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6091296","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6091296"}}}}}