{"entities":{"Q7030922":{"pageid":21688422,"ns":120,"title":"Item:Q7030922","lastrevid":77531078,"modified":"2026-05-04T20:48:53Z","type":"item","id":"Q7030922","labels":{"en":{"language":"en","value":"Certified first-order AC-unification and applications."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7980989"}},"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":"Q7030922$881478F2-F490-4917-B42D-6CBB7539D40C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"62a311c00e526a828e5a18acaf5879d4dddd2a82","datavalue":{"value":{"text":"Certified first-order AC-unification and applications.","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7030922$037F2FF3-D400-4E34-963C-12DDD15802C3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8b0e6ed1aec68796bc65bc4f158a64dbf7c39d0d","datavalue":{"value":"1557.68083","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7030922$064ADE51-A426-4797-9883-260721A952F4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9423fac0e1c2bf0265d53de8bc42e77d676ca060","datavalue":{"value":"10.1007/S10817-024-09714-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7030922$6D717065-7338-4DD6-B494-1021DB2F5677","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb39c66b74dd471ce57c28215b275dfb915aaaa4","datavalue":{"value":{"entity-type":"item","numeric-id":529653,"id":"Q529653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$F461C491-C588-44E4-BEE3-5EE1257EAF77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e491443c7df26a4927a70e826f0ef916b7e0bcd1","datavalue":{"value":{"entity-type":"item","numeric-id":405749,"id":"Q405749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$E44D7906-CB44-4116-80FA-A4E2A5660E23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8864d713270d3cb091c2f1ef2f7846d0d47fa57c","datavalue":{"value":{"entity-type":"item","numeric-id":5022929,"id":"Q5022929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$522686DB-29BD-445C-8F4D-2B60DDEBEB85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"22aae427d987903b086f7261fd1e4d8ee37a346c","datavalue":{"value":{"entity-type":"item","numeric-id":351994,"id":"Q351994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$E38D2F23-653C-4E6F-8BA8-EF3347FCF0D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a780894b40753623b223e1278bb24d0df726e149","datavalue":{"value":{"entity-type":"item","numeric-id":683745,"id":"Q683745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$4F99ED30-A930-4A0D-AA9B-6153AC9A8560","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$504D07C7-8C26-4700-9E44-2C18531D29A3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6451a7084150e57d8187f13df3637bcc3e62c7d9","datavalue":{"value":{"time":"+2025-02-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7030922$27058020-5634-4824-A5B0-6F4BAE9A405C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7030922$22B27EEE-4260-46FE-B00D-DC829A43D52E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7030922$9C7BF4FA-ECD9-4755-9EE0-E660A8F559F5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d52fc8ddce1ef9af3b31a96e3818875b53c3c2df","datavalue":{"value":"7980989","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7030922$A6BD0274-A06C-40D4-B720-4802B8C41944","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e1f8ad86efdaf8997a501e2aaad7c7a4ba85cdc7","datavalue":{"value":"AC-unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q7030922$AA4F6BAD-09A1-4865-A6C6-5FBA91B6A389","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3d3d0d2409011411be91984a4137a1c90ca04ff","datavalue":{"value":"PVS","type":"string"},"datatype":"string"},"type":"statement","id":"Q7030922$081394E3-0BA9-4073-9721-72E1695E3098","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eedb7896534a85540b0afa0d8982e6653023fca0","datavalue":{"value":"certified algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q7030922$FA305C18-55B0-491B-A78E-83FE38496E23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q7030922$BD50560A-6C02-4FF1-9090-AC9CEEAED3F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q7030922$EDDE677F-1E0D-4875-BE0B-8CD0A3026047","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":"Q7030922$8D0D9C5D-3F2F-40C0-A156-89C0BD00248D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2ab94b3ebee736752d1d28932367261ade31626","datavalue":{"value":{"entity-type":"item","numeric-id":1199708,"id":"Q1199708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$10C6959A-615C-4116-B7B1-2F8A22BB5544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eba843c99ea191eefc105c3cafc827293c69e422","datavalue":{"value":{"entity-type":"item","numeric-id":6544100,"id":"Q6544100"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$2D53C1E8-9C0F-40FE-A4A3-AA660014B2D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4cecf39dbce940c58e40445d47d899d6f66b714","datavalue":{"value":{"entity-type":"item","numeric-id":5369476,"id":"Q5369476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$CC5A332A-44E3-4EAF-9BFB-EAACB5FB8EDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1ca8fbf23bb44dcb11d380b98a2e7e3c9a4903b","datavalue":{"value":{"entity-type":"item","numeric-id":1744405,"id":"Q1744405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$B588DEC4-6332-4607-9913-BC30ABE8EDBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d55b861e5da5a0b09cfc74cd6df9a847a0d552e8","datavalue":{"value":{"entity-type":"item","numeric-id":2424886,"id":"Q2424886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$1FA5B087-0381-400F-B6AA-ABB5C9079721","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"523969521351e922268601919badf5f95b6cdd41","datavalue":{"value":{"entity-type":"item","numeric-id":5022930,"id":"Q5022930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$A9ED15C1-D5D2-4E2F-861C-FC67D775A475","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36b098b25d97e4ddaff4bf6a228f01587879d00b","datavalue":{"value":{"entity-type":"item","numeric-id":6118812,"id":"Q6118812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$452DBE42-06C5-479E-9D71-135ED15B630E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$6D30580C-DAEA-4647-BC2A-AA3806FD4F9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"becf5f4cc735947b117fb82f7aabc6a54df59ef2","datavalue":{"value":{"entity-type":"item","numeric-id":1099615,"id":"Q1099615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$53B8AE71-10FA-4F92-9902-C0B90256A24A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"406f53286fb764672117128a2d1f5fe44e5c8604","datavalue":{"value":{"entity-type":"item","numeric-id":1319390,"id":"Q1319390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$22F4E361-4C74-4400-899D-671145A70E47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2146fe71b39638fd1364e80615a2a1a9ddb51fe","datavalue":{"value":{"entity-type":"item","numeric-id":5313189,"id":"Q5313189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$71FA7594-A4FF-4D0A-B3F9-C7D4AAF16C55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b4861404e50c5efca67ce9accf62570167fdaba","datavalue":{"value":{"entity-type":"item","numeric-id":1121310,"id":"Q1121310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$1EFEEC69-28E9-4305-977B-F8C7C36BA1BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5dc32522e0062cccf7ff7280961b0c091134e3a","datavalue":{"value":{"entity-type":"item","numeric-id":5901563,"id":"Q5901563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$4650402A-950E-4FF3-A905-5A871CA08916","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86415c654a903509b73bb5d92c7a2bf96bc67567","datavalue":{"value":{"entity-type":"item","numeric-id":2104541,"id":"Q2104541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$CC33443F-5C35-4C39-8E3B-9F0F4D367B21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"052186b747d379b95536dd183092a6d28a9a4c59","datavalue":{"value":{"entity-type":"item","numeric-id":3338216,"id":"Q3338216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$8FE7EB53-805F-4462-B739-FEFD923324D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271f4a7c2003a89ce24a1f14fd1296133af596ac","datavalue":{"value":{"entity-type":"item","numeric-id":1099648,"id":"Q1099648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$621E738E-EA51-4EA6-934D-071143B19930","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9461b8596f936b4acd4b9ccaf6444d9340797391","datavalue":{"value":{"entity-type":"item","numeric-id":2373703,"id":"Q2373703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$13F50F6E-AE20-40A3-8D21-913E8925D927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b18f9bdbc78d3b714191d0769b308a9a6419132","datavalue":{"value":{"entity-type":"item","numeric-id":5747641,"id":"Q5747641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$22099CE0-75A3-4675-B147-C4CB656CE799","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d37b23b7db99d33ba41b8c893bcac4aca2de8fdd","datavalue":{"value":{"entity-type":"item","numeric-id":4870018,"id":"Q4870018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$5CA16191-3951-401C-A0E1-FA8E73A91782","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9863219edf0cf338b34eac05af7eeb8c6f738697","datavalue":{"value":{"entity-type":"item","numeric-id":692371,"id":"Q692371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$F89B1B58-07BD-4CAD-A9B7-D2A57A48D037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d4132baf3bef4595b4215c4d575f32e9fdd719c","datavalue":{"value":{"entity-type":"item","numeric-id":1791187,"id":"Q1791187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$0794D4B6-608B-468A-A7F4-DBB623480906","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d7c974da2fbdfbb494f4ddce13bd1f1e2231832","datavalue":{"value":{"entity-type":"item","numeric-id":2849600,"id":"Q2849600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$9922B547-5B01-4329-9E74-62629CF2666C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1669261077901413d76dc0f7072dfdae93141a3b","datavalue":{"value":{"entity-type":"item","numeric-id":3912070,"id":"Q3912070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$D679CDE2-FA5B-4507-86D0-DF524B336AC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ade402c8643377c95736cc4de881776c386a1875","datavalue":{"value":{"entity-type":"item","numeric-id":1882909,"id":"Q1882909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7030922$70F37438-82F3-4126-8532-E0ED5DC10635","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Certified first-order AC-unification and applications.","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Certified_first-order_AC-unification_and_applications."}}}}}