{"entities":{"Q3454097":{"pageid":5233497,"ns":120,"title":"Item:Q3454097","lastrevid":58181463,"modified":"2026-04-04T03:27:46Z","type":"item","id":"Q3454097","labels":{"en":{"language":"en","value":"SEPIA: search for proofs using inferred automata"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6515510"}},"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":"Q3454097$BFF7B4C8-09AE-436B-896F-352137B7DC9A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1b1767008dd2aebca8fabd4737c367fe2e473797","datavalue":{"value":{"text":"SEPIA: Search for Proofs Using Inferred Automata","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3454097$5B8A306D-8D98-4BF3-B4A6-7B9780207E19","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"832bd021f91c934b768f16ae7e2f2ba5f9ed3e6d","datavalue":{"value":"1465.68284","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454097$9386849E-8A73-4255-9B34-AB36BB379125","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4f4fe55f2565dfa1d43300fc7d234f4e46aa0184","datavalue":{"value":"10.1007/978-3-319-21401-6_16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454097$0EB06E3A-A8EF-434A-9A8D-8CFBE39F814A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8877e077324af18c56acae783fb9d2b80c908654","datavalue":{"value":{"entity-type":"item","numeric-id":3454095,"id":"Q3454095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$6B7D40B2-A630-4E4A-8A0E-529005EC5DF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b4766a06aa052db7f2e5b400a1accd823e3573f","datavalue":{"value":{"entity-type":"item","numeric-id":3454096,"id":"Q3454096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$0321CEB7-58E1-4846-B3A7-0688AB4F5206","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"db0628f44775a176dab1adaaf7efe9aff6d9aed4","datavalue":{"value":{"entity-type":"item","numeric-id":294928,"id":"Q294928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$110CF494-5710-468D-8E9E-2C12412AACEC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3cc4c7edeb37e5e3024aeff0de74501df6e066e3","datavalue":{"value":{"entity-type":"item","numeric-id":3454078,"id":"Q3454078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$2F6693C8-ACB7-4351-B8CE-8BDB99E264A3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f34c33daac76be2878f4eb0eeca7aa927e679a8","datavalue":{"value":{"time":"+2015-12-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3454097$4A44D340-955A-41BD-AE7F-245F7D3F5AD0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e64ebc15008d19ab9e6b5af56081f6b93a14d23f","datavalue":{"value":"https://arxiv.org/abs/1505.07987","type":"string"},"datatype":"url"},"type":"statement","id":"Q3454097$E78544B2-A1A4-4D06-8195-6FE4C4320FAD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454097$EDEBEA5B-8448-41D5-B66F-76BE510195BB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f59c477311e6048efecbf3e9772f20c2ae2b3e2d","datavalue":{"value":"6515510","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454097$84298EF1-3AEF-4352-B203-74C92C0EE999","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3454097$CBAB3C41-D4DC-48B9-9354-E650A976FB42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c602ea7429f09bf06b78b5990f80ab873b869afd","datavalue":{"value":"model inference","type":"string"},"datatype":"string"},"type":"statement","id":"Q3454097$39EAAD95-F6E1-4CF0-BF9A-784D2E720300","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d62798ced101241ac0d5e46110e32d69e73a0c1a","datavalue":{"value":"proof automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q3454097$B9283F04-8471-467B-8079-E6F74794F90F","rank":"normal"}],"P1463":[{"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":"Q3454097$8CD17339-0A67-4587-910E-3DF0765EBF69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$849E174B-AC8A-45AA-8521-AAD0F10B1FB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0ecee973cce27aca9d6609100a6fb4d87c282d91","datavalue":{"value":{"entity-type":"item","numeric-id":19195,"id":"Q19195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$04E992B8-1CD3-4807-A5E9-E1893FFABCDD","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":"Q3454097$4623AC48-916A-424B-BC19-3B36B4B5A434","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"60dd00d4555f8bb2bf4742d7e369d9f6e2f1ccc1","datavalue":{"value":"W1581101260","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454097$2FCE0643-C90D-4CB8-AE2F-0471DAB1E658","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"065f96a47cd2c09ae1ea2ab42886a32d0c8223cd","datavalue":{"value":{"entity-type":"item","numeric-id":2891438,"id":"Q2891438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$51E08776-F940-44CE-929B-C4647567A391","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$2085BC43-A00C-4BE7-94B8-0AEB7592D799","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fbfe7d7615014fafe2898a7e08fc2bf421ac549","datavalue":{"value":{"entity-type":"item","numeric-id":5495930,"id":"Q5495930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$82B95028-79BF-40FB-992F-E2F3986AFDBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d338e06cf9942819965d2c816cc3ef86f90f016e","datavalue":{"value":{"entity-type":"item","numeric-id":4465166,"id":"Q4465166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$C4A4EE62-9851-44E4-8A3D-DAA8F97909F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$45E1BBDA-AFFA-49AF-ADE2-FB61D6D91F09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b5045e17431ae100adc29ee6860720ac72d87fa","datavalue":{"value":{"entity-type":"item","numeric-id":5302561,"id":"Q5302561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454097$F1F0DEDE-3556-49B7-9ABA-4C350D289CD0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00791ad6732504b73968cf763a5aaf468fc85584","datavalue":{"value":{"entity-type":"item","numeric-id":5495930,"id":"Q5495930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ce9483c83466a056a63a7b35f21a61c971544ee","datavalue":{"value":{"amount":"+0.7580738067626953","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":"Q3454097$A63748C8-743F-4109-B474-773366008F26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68b122fc17cf6c180e33e2295f43b455fdd3224f","datavalue":{"value":{"entity-type":"item","numeric-id":2219409,"id":"Q2219409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbb984f523f4f4a607070f7321a8b6c2e3591870","datavalue":{"value":{"amount":"+0.7178935408592224","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":"Q3454097$4AE66970-8A16-4427-9FD0-EC198F1EC432","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b7ac36ed718b6e97928eb57ef2af05bff63f6d3","datavalue":{"value":{"entity-type":"item","numeric-id":5398327,"id":"Q5398327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9e57ce06aaf637f92ea696472ebafaf23853730","datavalue":{"value":{"amount":"+0.7176451086997986","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":"Q3454097$B1400AA7-88DD-45AF-9151-7A72BF9CF44B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e991eb6ce62deb5bb2a8abdd6157fc56a8e6e1f","datavalue":{"value":{"entity-type":"item","numeric-id":5176973,"id":"Q5176973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66e163840a7198d19d5b826043bc13d501b52623","datavalue":{"value":{"amount":"+0.7176447510719299","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":"Q3454097$71F6330F-6ACD-475C-BE6F-9215333ADDA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14b8b36929715000acf1cd883b9b1d7bc9f1ba30","datavalue":{"value":{"entity-type":"item","numeric-id":475385,"id":"Q475385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7dded5935d88176f2dc46d2120caa02b18685cfd","datavalue":{"value":{"amount":"+0.7112250328063965","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":"Q3454097$8E2E5A12-65C4-477C-B2DF-321EAF0144CD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3454097","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3454097"}}}}}