{"entities":{"Q40285":{"pageid":40341,"ns":120,"title":"Item:Q40285","lastrevid":105428150,"modified":"2026-10-09T10:09:10Z","type":"item","id":"Q40285","labels":{"en":{"language":"en","value":"Superposition Calculus"}},"descriptions":{"en":{"language":"en","value":"AFP entry SuperCalc"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"7d3a837ea720f21051c4c89c63aa04a479f75c20","datavalue":{"value":"28571","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40285$70E71A28-B265-49D9-8657-96955C82CFDC","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$BA2FA4F3-A432-44F9-ACA6-C6CD4CC3F9DE","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"06890a57c640def4326fa6acec07c21825daf0ea","datavalue":{"value":"https://www.isa-afp.org/entries/SuperCalc.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40285$1B716125-4BA6-4975-BD15-628F1AA381F1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40285$441EAD13-F2EF-4651-A4A1-68C5D6FE7C93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40285$26F9C031-9D13-470D-B156-B2D3D337A0C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40285$4DA6FA3B-7B3E-475B-A0CF-B9DCD1F92E52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40285$689E5D83-E437-40D7-8484-0D412B1C7BB7","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$3DB5DAF6-46F9-4C5A-9193-1F1F6671FBBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$1B90879B-0DA7-433F-A208-205757A30D86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$C6512B3A-469E-4072-A000-F7B466C6B6E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"28fc316ccc1f38bd6830fcffe3187b6d32168084","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$94B7A864-6793-475B-9B78-3FC9FAD930CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$B4F326C6-7FBA-4315-BF4F-235C6D7E7DFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a0a329d132b963c571723538ca5cd1b467b324fe","datavalue":{"value":{"entity-type":"item","numeric-id":40325,"id":"Q40325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$938CB09A-B502-4FB2-94DE-E03E538A1774","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9a2aad95369d69c08086a6600b609b3220c2705e","datavalue":{"value":{"entity-type":"item","numeric-id":40276,"id":"Q40276"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$30DD219C-371C-49B8-89BE-5CE36B43F741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"dc75b1f4f41a196c347c039c5eec89b08662123b","datavalue":{"value":{"entity-type":"item","numeric-id":18543,"id":"Q18543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$806C60D6-5BC1-4BB0-822A-744AF4D0EA20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$CFB242DC-BDCE-4F31-BE2F-9C27E402BCE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$56443790-620F-42CC-A313-B75DEE184CEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1c1111a4af73946d995c6025450c33305be35b38","datavalue":{"value":{"entity-type":"item","numeric-id":40350,"id":"Q40350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$59299C87-2EF3-44D2-B869-BCDB82F4FF7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f0874088d59a2cbce379152e0f60bc05817c8d64","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$88E36539-6FBC-4B49-B725-3CF5CF4F93AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d6d29b9e294eea1a26ce05a4d8663847cfc55575","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$CE866667-E3A5-4E75-B41A-FD3973242C9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"493c5144a9d14f0b980d45769fb4b197b51b453c","datavalue":{"value":{"entity-type":"item","numeric-id":40555,"id":"Q40555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$B9B1291D-D430-43C5-BD7A-CFF188E7AF04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0204f081facf570c6ab1a272475183b48ae5e4f2","datavalue":{"value":{"entity-type":"item","numeric-id":40286,"id":"Q40286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$11D2B9C9-FED1-4C2F-BA0B-C91626DCFD9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8bf2731143fd82a1f95f40f13b2fce56fbb7345a","datavalue":{"value":{"entity-type":"item","numeric-id":40299,"id":"Q40299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$B1AB72E8-4BD0-45E7-A4F3-D3D6DF861D7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ab75a27745b95bbc51eed60e2ef7157b7c449125","datavalue":{"value":{"entity-type":"item","numeric-id":33768,"id":"Q33768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$CA89088E-85D1-405B-BB43-65F6D983A9E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"861e34f6b532f04d877297070a58fb137923d509","datavalue":{"value":{"entity-type":"item","numeric-id":40509,"id":"Q40509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$9DA6A3FE-0041-4B7E-9B33-8F095D7185C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a3d1e0e198e45cd480c75f3cdc16c51aa12a9827","datavalue":{"value":{"entity-type":"item","numeric-id":43931,"id":"Q43931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$16305B4A-CE98-40C7-9978-7EEC30AA0A59","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"920db1fce8ddde3188f98fdde7e78f68ffa40470","datavalue":{"value":"https://isa-afp.org/entries/SuperCalc.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40285$3DED7D74-F29C-476A-8FE4-18B9A4D82849","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"c428ef8e1c5808ff44cb31409c13e26666127c32","datavalue":{"value":"Nicolas Peltier","type":"string"},"datatype":"string"},"type":"statement","id":"Q40285$57449454-66D0-4116-AC41-4EA2D77D1FC4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"9229bb27b1c357535e19f00087e1625c0be3649e","datavalue":{"value":"We provide a formalization of a variant of the superposition calculus, together with formal proofs of soundness and refutational completeness (w.r.t. the usual redundancy criteria based on clause ordering). This version of the calculus uses all the standard restrictions of the superposition rules, together with the following refinement, inspired by the basic superposition calculus: each clause is associated with a set of terms which are assumed to be in normal form -- thus any application of the replacement rule on these terms is blocked. The set is initially empty and terms may be added or removed at each inference step. The set of terms that are assumed to be in normal form includes any term introduced by previous unifiers as well as any term occurring in the parent clauses at a position that is smaller (according to some given ordering on positions) than a previously replaced term. The standard superposition calculus corresponds to the case where the set of irreducible terms is always empty.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40285$42488EA7-126B-422C-9CD0-5F686AEDBEDC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$D6B3F788-A04E-4789-B04A-E4E2D449D603","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"309a715ecfe3fe3e4ec0e698ae13dce021cfc93e","datavalue":{"value":{"entity-type":"item","numeric-id":2724150,"id":"Q2724150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$53935A17-9543-407E-B695-D70C75E3E434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f14878b4342799995051ac9bc54cd21c98efc98","datavalue":{"value":{"entity-type":"item","numeric-id":2751359,"id":"Q2751359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$0DA29613-E660-4674-97B8-3DDC6C91F49A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97ba68be7d715061cf7a668b6481e26fa5a74409","datavalue":{"value":{"entity-type":"item","numeric-id":1305166,"id":"Q1305166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$EBE3426C-2072-4180-9A2E-60C9975C94E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e38c2f2e2ea48fd30061f5b3a3a8d0dacb950761","datavalue":{"value":{"entity-type":"item","numeric-id":4264723,"id":"Q4264723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$C457E313-7EB3-4A19-A4EC-13FE462BB40E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ad7c23e8d7895495a33ef0a244c1d5f7a7d7e16","datavalue":{"value":{"entity-type":"item","numeric-id":1899908,"id":"Q1899908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$31607498-25F2-4CE8-922B-4B9D7CE6188A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ac29eae65679ec4daa83250ac6240c854e9b22a3","datavalue":{"value":{"time":"+2016-09-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40285$C7A4D0E1-6A13-41CD-A37F-02ADA68F33F0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"512a53991a761ecd4142db1761fa8231d5b16dc2","datavalue":{"value":{"text":"A Variant of the Superposition Calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40285$00683090-B210-4EFF-AA7B-1363FD248F05","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$C0A616E5-3FAA-43A5-AD89-73B856683DB7","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"0010e22d998484f218097f7f79d7fc22bc7427c6","datavalue":{"value":{"entity-type":"item","numeric-id":7360817,"id":"Q7360817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40285$A67F91F9-D64B-482E-A1EA-8A0CE27604CB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Superposition Calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Superposition_Calculus"}}}}}