{"entities":{"Q438531":{"pageid":440298,"ns":120,"title":"Item:Q438531","lastrevid":51520304,"modified":"2026-01-18T15:00:42Z","type":"item","id":"Q438531","labels":{"en":{"language":"en","value":"A combined superposition and model evolution calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6062047"}},"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":"Q438531$52063F09-EDBA-45E2-948F-A32AF7A2D972","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fafb045bfdaa2f054b99d372c220ac6bea7bbe54","datavalue":{"value":{"text":"A combined superposition and model evolution calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q438531$371BF676-DD46-4196-BBC4-345F119B48AC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ca02b2030e5d9ba84d1f8df3a66d9ebcdee53694","datavalue":{"value":"1267.03033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438531$124717B9-B73D-48AB-9A62-609FD2C37455","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ecde3ddf4f96a8da457aeb906b2979614b354694","datavalue":{"value":{"entity-type":"item","numeric-id":293310,"id":"Q293310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$C8A09B31-411B-4BBC-91CD-FDC6F76ACE1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"63095d86c000f08026b5823fdf1f8a25bfef2e00","datavalue":{"value":{"entity-type":"item","numeric-id":167057,"id":"Q167057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$A16A60EB-FFA6-4C5C-9270-01FD72BAD016","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":"Q438531$BDEF5045-9705-41F0-B614-577498E28384","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c7ad691786690cf86127845d28cf47311748286","datavalue":{"value":{"time":"+2012-07-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q438531$55F94AAB-2925-4BB6-B721-096265F1E865","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7a3ce43b5c2047ffa1c671987937a612e7e5abd0","datavalue":{"value":"The paper presents a new calculus for first-order theorem proving with equality, which generalizes both the superposition calculus and the model evolution calculus (with equality). This calculus integrates the inference rules of superposition and of model evolution preserving the individual semantically-based redundancy criteria of both calculi in a single framework. Moreover, this work simplifies the presentation of the model evolution calculus by using the better-known superposition framework. The main result of the paper is the completeness proof of the calculus under semantically justified redundancy criteria and simplification rules.","type":"string"},"datatype":"string"},"type":"statement","id":"Q438531$C0D60E53-8F31-4E5E-85C0-A171CE4D7F46","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"f47d936c4ff4164197e28a1ea38124145d11538c","datavalue":{"value":{"entity-type":"item","numeric-id":313005,"id":"Q313005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$3AEA0028-6076-4693-9E1A-BFB98D344EE4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438531$11B965BB-7CAF-4ECB-A0CD-F525D52A7073","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438531$7C89AA6A-5F93-4263-A268-B0968F040DE3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"439eabb111577dee30f747fcaf507c4e48d78242","datavalue":{"value":"6062047","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438531$23026B9A-104F-47A7-BF85-671B2FB0C540","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6dd547626f7f61a5a377a5c5f0922b8194538c7e","datavalue":{"value":"instance-based methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q438531$65920C08-23CF-4492-BB8B-4D97A670AE34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d86a171fa82c1ea15db4e7a7c23402cbb117f3b1","datavalue":{"value":"superposition","type":"string"},"datatype":"string"},"type":"statement","id":"Q438531$A6F438E8-A9D9-4FDB-9B2E-8C41712B10B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a3a17a8def65c80d2fb505b88fa0285e75b25268","datavalue":{"value":"model evolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q438531$28DCCBE6-F936-477D-98CF-5425C43EBA80","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$585295E6-732F-428B-B404-9417CA7C066D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"83e2dec25ea583652d0e07d4393a843812f4b48b","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$CBA28F04-F0BA-4DD3-AD76-CEE07B0162E8","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":"Q438531$2457AC39-75DD-44F0-8A96-28795594DBD0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"61f1c71989959382191f69a8a12c44ca3e5e0f4f","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9214-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q438531$310AD007-C042-4172-A204-184A8C09EFE7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1ae4be12fe7081695ea6bc3299be3816f1348612","datavalue":{"value":"W1965168302","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438531$637B9EA6-D6F7-44D2-BF74-D49FB842C243","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"49666558e5a266f8c31a331a000db76b0e587406","datavalue":{"value":{"entity-type":"item","numeric-id":4524792,"id":"Q4524792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$73D1E364-67F7-4695-8A16-A46EDD8C272D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4db61376dc05e8ac9b799b75f45910b0e723393","datavalue":{"value":{"entity-type":"item","numeric-id":1328182,"id":"Q1328182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$136E2932-773F-4C07-9744-BA4BF13ED2DD","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":"Q438531$A32FEE24-D7DB-4F7F-A993-17CF04D91EA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b07bee7e03caec103786e5014f6d4794b8bbdd6","datavalue":{"value":{"entity-type":"item","numeric-id":5900727,"id":"Q5900727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$A14456A8-F368-48F3-BADA-0F45318E8753","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3fc0836acee68f0bfd8ffa99e594e42d0f2ccbde","datavalue":{"value":{"entity-type":"item","numeric-id":5394627,"id":"Q5394627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$0BE447F4-F101-47F7-8904-A0AF87F8EDC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae611ccf26d614d6f5569c32d95f83372cdd7983","datavalue":{"value":{"entity-type":"item","numeric-id":5311286,"id":"Q5311286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$8A34599C-AF61-4F1A-9185-8D3B873EB32E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0cec2b5bcd3b5bad2cdc0fa09422f09cc364dbc","datavalue":{"value":{"entity-type":"item","numeric-id":877884,"id":"Q877884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$7549080C-DF0C-4378-9D1D-8BB0FC4D5926","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33890b7faad584193275d91a4cd4d3b147aff5a7","datavalue":{"value":{"entity-type":"item","numeric-id":3541709,"id":"Q3541709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$1F782C13-0032-4EE9-9123-9C02D9F4F35B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8d0a313e4a8c081157c7381bf73a04563a6d396","datavalue":{"value":{"entity-type":"item","numeric-id":3655208,"id":"Q3655208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$B4D30D92-AE6C-4B7C-93DD-EB6A1B6FB2DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78a8fb7c1504b4023b489475633410efba01eda3","datavalue":{"value":{"entity-type":"item","numeric-id":1897557,"id":"Q1897557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$5DAEBED9-99B8-4627-B718-4648289192E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f00589542fdb6ec4fc401e47318165d5bad4f817","datavalue":{"value":{"entity-type":"item","numeric-id":1581853,"id":"Q1581853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$27F882E6-B32B-446B-8EF3-6F6743DCEB6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"842d1c2c50e4f6152c1646f7649b15d27250c7c8","datavalue":{"value":{"entity-type":"item","numeric-id":3608799,"id":"Q3608799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$E0371904-8AB0-4EA7-B588-4FCC9FE1A47F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98e3de5ec781152a1fb4ad1c034316f4f1bf1581","datavalue":{"value":{"entity-type":"item","numeric-id":5394610,"id":"Q5394610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438531$7015653F-ACBB-49AF-87D1-BF6451B8D987","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3f04e4c18f0505025a0dd25878d6310cf2c8a35a","datavalue":{"value":"10.1007/S10817-010-9214-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438531$E2F60565-0697-44A8-B100-4543856FED9F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7e1710ded83e70542233b4417eea911ce3e3a0af","datavalue":{"value":{"entity-type":"item","numeric-id":5191094,"id":"Q5191094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"39eedbc75cddf929da16fd57b0594b747d68fb24","datavalue":{"value":{"amount":"+0.982978343963623","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":"Q438531$530C70AC-0C78-408B-BC4A-B193F0E9C3FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c2552b0abed1d99e9628732a5ea40988e1006f66","datavalue":{"value":{"entity-type":"item","numeric-id":429586,"id":"Q429586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6e5a2a0884f0c95200df3d28498662fd7a1a7fb","datavalue":{"value":{"amount":"+0.8522059917449951","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":"Q438531$A281F109-846A-4B5C-841A-6E144F35DC92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3095e6f99c1ed9ba385376092c408fc254cedf90","datavalue":{"value":{"entity-type":"item","numeric-id":5394627,"id":"Q5394627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed58fa13f7f7b4cd02f7b9b51f344d48dd290484","datavalue":{"value":{"amount":"+0.8491074442863464","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":"Q438531$3EB80CBC-A39B-4BCE-82FE-BBBB50C889A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6469e4035f4b33be56f6094cde9f019c584fe8b9","datavalue":{"value":{"entity-type":"item","numeric-id":4412856,"id":"Q4412856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"052e79f5d4136c2e64319e9886989fed4aac56ae","datavalue":{"value":{"amount":"+0.8132632970809937","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":"Q438531$AF4F87E0-D12A-4950-A078-B367883E0909","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"74e87f21cf6895604b90a73a0ae842ada1e904ac","datavalue":{"value":{"entity-type":"item","numeric-id":2352496,"id":"Q2352496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04a86c6a99efd0c170a58c229e648979317504a0","datavalue":{"value":{"amount":"+0.8114690184593201","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":"Q438531$25B1B13E-B9B6-446B-838E-FDF579A17836","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:438531","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:438531"}}}}}