{"entities":{"Q4647573":{"pageid":6677154,"ns":120,"title":"Item:Q4647573","lastrevid":53321216,"modified":"2026-01-24T17:45:06Z","type":"item","id":"Q4647573","labels":{"en":{"language":"en","value":"Automating inversion of inductive predicates in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7002047"}},"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":"Q4647573$303E53D9-074D-4CFE-971E-7685617F2E5F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bb66389c679bd52cd66dbab6fd3bf8ca04d0a7b6","datavalue":{"value":{"text":"Automating inversion of inductive predicates in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647573$13317FAE-F841-4208-9407-5883D727E92F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6ad7ef8a1bfadc931a26b51e6faafd9f5f44bc5d","datavalue":{"value":"1407.68433","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647573$C24E7A70-0603-4A36-9E06-C169E8C221D5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e46fdd22e680fd90d28afb399f2823474190b909","datavalue":{"value":"10.1007/3-540-61780-9_64","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647573$7DFC4505-7D89-4EC6-8DAF-F886157E2CD9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6528ead9d378ea8de58749e8c1892c24bb577aa7","datavalue":{"value":{"entity-type":"item","numeric-id":2766800,"id":"Q2766800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647573$97A77C0D-83D5-4DA7-9E9E-1315F0E46C30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bcd59f4149a9afe4198ea3498fce8a2983db1f42","datavalue":{"value":{"entity-type":"item","numeric-id":4647572,"id":"Q4647572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647573$20FEE1B0-184C-42DD-8D08-AC34A0DA346C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647573$1B4FEED7-41EA-493F-9755-D3788E2FE1EB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647573$2E4B927A-5832-4D84-8A61-1154B6733D3C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647573$2B07F31C-03C9-4196-BAA2-308193248726","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b492f281b8f52c724f2bc547e7e570cccf4bd5e0","datavalue":{"value":"68N17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647573$72017973-DC8D-43F6-8CD2-12C6C04A6522","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"196596a18a5b2dce57668b7ed4b426e00eda94f5","datavalue":{"value":"7002047","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647573$D20A5BE9-2899-4591-A76C-35C6EC79D10A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"91993be004af1453cf4fd79c07e1ba49b9211805","datavalue":{"value":"logic programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647573$123A7434-2E1E-448F-9788-BD0BE39E31E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8f384098e8f2ae4ef2ba4576b8d375f29034500","datavalue":{"value":"Horn clause","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647573$F97F65E0-F1E6-4C18-8FFB-475D5634516A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647573$0F2639F9-200A-45F8-ACB6-EBB98AC5B488","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ed28ff65c7143ccab364c3b93115be1e84f3431a","datavalue":{"value":"inductive type","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647573$8D77BB38-D9BD-4918-BD81-A672E50DAE4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba29bc695092e1012b615eb49ec43774f5b5c42a","datavalue":{"value":"inductive definition","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647573$BBAB5EA2-C502-401E-BB4D-63D1CDDABAB5","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":"Q4647573$C8AD7AE6-7115-4AF5-AB47-2C99DD0A06C6","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":"Q4647573$BBD33DDA-8FE3-4CC0-A90E-1856C5B952E9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d734aa51252c27324929d49d0a4e9383fbcda5be","datavalue":{"value":"https://doi.org/10.1007/3-540-61780-9_64","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647573$4D1B41B2-B52C-4571-9988-CF3C8C9A7ABF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"650d3fc89e61983670d58912205fcbc6e72c73cf","datavalue":{"value":"W1849370879","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647573$6AACB0E1-845B-4A75-8F16-724EA2B7B076","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647573$16BC9CCB-9765-4D66-AAE2-CFBCA4C2E424","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05ea7e81c6de0065717c066fc903d6beef24bc1c","datavalue":{"value":{"entity-type":"item","numeric-id":4647573,"id":"Q4647573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647573$D7A273F2-235C-45D0-AB97-670E370D3F43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37bc8dae1994f1675072ec162c7c6788e05d8d41","datavalue":{"value":{"entity-type":"item","numeric-id":4296744,"id":"Q4296744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647573$0041B429-F924-4623-9BAE-2E406511431C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b67f62053c0da9e304f60e65a89efe6ab3bb050","datavalue":{"value":{"entity-type":"item","numeric-id":1346629,"id":"Q1346629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647573$3186BDF4-2D57-4A75-B26B-36D3AD8244B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647573$DC882ED4-8D8A-4658-B455-3A274B8CF62F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2dedeed48f478c18f307fcd52efdae3106a782b","datavalue":{"value":{"entity-type":"item","numeric-id":3543650,"id":"Q3543650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb5a3fa66bdce8f906510e9c1a6457a4b10a1f10","datavalue":{"value":{"amount":"+0.7912592887878418","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":"Q4647573$F9D98D2A-6A69-4933-9F8F-B97DFB2F4BE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aeea8e1b74f93b4eadc94e67aafe59d3632e9350","datavalue":{"value":{"entity-type":"item","numeric-id":5327354,"id":"Q5327354"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9338cb76f271f6d3c37e0529d24e8af042723941","datavalue":{"value":{"amount":"+0.7475742697715759","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":"Q4647573$254F730E-4487-4B83-8E3E-1B1C005ABBF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0d7e5f8e13bcfad3b90deb880cccfde5e25fd42","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e09b5bb52b4d6726e2be58118f8c00216c79030","datavalue":{"value":{"amount":"+0.7348009943962097","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":"Q4647573$84BE6C1E-6D82-4B51-B722-D07803F917F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ed7d1c79c5d9622e1eeadc1aaf2b3855954e4971","datavalue":{"value":{"entity-type":"item","numeric-id":1824382,"id":"Q1824382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3003b826eff1d0becd65d22bbc82ef2dccfd33f9","datavalue":{"value":{"amount":"+0.7255746722221375","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":"Q4647573$F916B51F-9310-4603-8AFA-2C76B4E817E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6bdf3dcf99bbb982c90981d2d4af8778dfd4e454","datavalue":{"value":{"entity-type":"item","numeric-id":5712312,"id":"Q5712312"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"14e93ae01afa3560f4f6f7f29efae14172425f97","datavalue":{"value":{"amount":"+0.7184924483299255","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":"Q4647573$41F6AE72-96EF-4319-8D8F-E131DF2B1E5F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647573","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647573"}}}}}