{"entities":{"Q1577484":{"pageid":1588224,"ns":120,"title":"Item:Q1577484","lastrevid":72234600,"modified":"2026-04-14T03:31:29Z","type":"item","id":"Q1577484","labels":{"en":{"language":"en","value":"Deciding the \\(E^+\\)-class by an a posteriori, liftable order"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1501507"}},"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":"Q1577484$4AC21BD1-CFF9-4DD0-92AA-81E59A3073F7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0e6b14481e4b2cd286306f418bb991fab5a22f10","datavalue":{"value":{"text":"Deciding the \\(E^+\\)-class by an a posteriori, liftable order","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1577484$5906D14C-AA82-42A9-907C-17400D1EC7DC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b29b50b0c1728a85add4f48550501b454fd20a39","datavalue":{"value":"0966.03012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577484$19503572-A22D-49ED-B499-ADF41237A73C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e61f313aef2f260f9c3dc41727fb30bea44a6e01","datavalue":{"value":"10.1016/S0168-0072(00)00013-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577484$B4DC161F-CF3F-4C2D-A88D-AF0696D0068F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0af7e025189305bad11f686c710fe3b187470eaf","datavalue":{"value":{"entity-type":"item","numeric-id":438567,"id":"Q438567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$90401E42-C0EE-4E37-AC5A-B14FBFB334F8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$42484D2E-37B2-4CF9-BE80-1E0C4767369A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b450668c82a8cd1fc850a44d0109b0a4a4df4467","datavalue":{"value":{"time":"+2001-07-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1577484$F40E553D-7340-41EB-9C1E-2D2C921AB0EA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"34f5823b304bc308501a40d26ca0b2740c29d5eb","datavalue":{"value":"Resolution decision procedures make it possible to use proof-theoretic techniques in an originally model-theoretic field.    One of the classes decidable by resolution is the \\(E^+\\)-class. This class is defined as the set of clauses in which all literals have the same set of variables, and are weakly covering. The author shows that the \\(E^+\\)-class can be decided by a liftable order after all, when it is applied a posteriori. Formerly this was posed as an open problem. The author proves termination for the full \\(E^+\\)-class, with a fully liftable order, and without saturation rules.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577484$542882D7-D1B7-429B-99E2-582401531E34","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577484$70AEC3F2-6977-4371-8D86-675209B811B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577484$84857862-EC9D-4A42-BA0F-8EDBB4893396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577484$9D9354CE-A8F0-4D74-BF03-002464B8074B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f60333fec1054da92f9057c590af335abaf51ec4","datavalue":{"value":"1501507","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577484$94C7D93C-B11F-4C6A-93F2-FC2ED2875908","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9097f5d131906574058554916f9f2c70fb78657f","datavalue":{"value":"theorem-proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577484$A58A2036-DE60-43FD-BCAC-681CF5F1D229","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8324f5b352cdba672f1154b8de6c235b04255eaf","datavalue":{"value":"decidable classes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577484$5A73D6E0-62E3-482D-99AA-A2A6AE3E761D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33230aef013e5fa671fa5be1b7ea4b93a52c1d57","datavalue":{"value":"\\(E^+\\)-class","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577484$83420487-B58F-476B-9C0F-6B680915C133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5f1e6cbb91f6fe42cdd2ea642ca0b50af01ce130","datavalue":{"value":"liftable order","type":"string"},"datatype":"string"},"type":"statement","id":"Q1577484$08477BDD-079A-4B30-B9F3-4941DC44895C","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"05f3dff3edc7d97b14af7ecb326f488fb3fee31b","datavalue":{"value":{"entity-type":"item","numeric-id":583186,"id":"Q583186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$60DCF6B5-E277-4E1A-A17E-3411B15D5203","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$99E922D3-4BD1-473E-AD0A-E2235C82006C","rank":"normal"},{"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":"Q1577484$D9847E4B-B0FF-4969-B2B2-031B33C40F54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f63de557d279c4616add6af7fb4f5f08e4cbf484","datavalue":{"value":{"entity-type":"item","numeric-id":41399,"id":"Q41399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$E8D72196-19F2-42C2-A4DE-B2CDA885A52A","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":"Q1577484$7C272770-B2B3-45D2-A86D-7F15B1A048EA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$79714B78-7F8E-4633-8AAB-41E0C4EA970C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da9035a3503d06ad7946ad5c060940ce1e7b476e","datavalue":{"value":{"entity-type":"item","numeric-id":3905252,"id":"Q3905252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$1484302F-E8A1-464A-9A3D-1C6CBFE5FE81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"315e95e4ad8a1c26487d3ff7728ab264483e45ea","datavalue":{"value":{"entity-type":"item","numeric-id":1310269,"id":"Q1310269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$DAE9448D-F58B-4178-9209-4297C6A9BE4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dda6d4bc4ff06358c5dfe216b9a7a58bec1514be","datavalue":{"value":{"entity-type":"item","numeric-id":4102765,"id":"Q4102765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$B8EC5932-C4C5-4177-B742-8F79AF922E8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8755fff25bcbf365d5dd2dfde2f78f833a2371b","datavalue":{"value":{"entity-type":"item","numeric-id":4331764,"id":"Q4331764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$9EEA593E-A340-47D1-A3CA-F16175273D10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1f163f4a3a9a5735632b1ba8e957c5e3573645b","datavalue":{"value":{"entity-type":"item","numeric-id":3728875,"id":"Q3728875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$B0542EB5-611A-4E9E-B67C-109DCC238EC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12ef7fe275e1013dfbbe27b73bc3de1034cddb1c","datavalue":{"value":{"entity-type":"item","numeric-id":4474846,"id":"Q4474846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$4D20F617-E188-4658-8BFB-B78CFD005D5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbd2b941917dce341ff718d83ae85a2cf999d6ba","datavalue":{"value":{"entity-type":"item","numeric-id":4249898,"id":"Q4249898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$C66C7754-0D08-4606-B3F5-7126C8D53D28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$27B9413C-0D88-4770-8C40-5E46F6117A6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"017c184c3277fb681aa54b180b0d3db5f9e6933c","datavalue":{"value":{"entity-type":"item","numeric-id":3348885,"id":"Q3348885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$8893B4E1-4D56-4F25-B8B0-6BC64B1EDB93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e963915702637e6f873c32169203d8b91d5f54c","datavalue":{"value":{"entity-type":"item","numeric-id":1217465,"id":"Q1217465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1577484$1C42D67C-D13B-4D1F-9C88-B5629DCB3C2C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e3120d216189b6bdf0286167c43dd51c20ba42e8","datavalue":{"value":"https://doi.org/10.1016/s0168-0072(00)00013-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q1577484$F4F472C3-4984-402E-B2DD-B336E63F9C85","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"603265907180d1079ca7bc2c8433ff367f5983d7","datavalue":{"value":"W2010309877","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577484$999FDB69-D851-49D0-AC65-B33B8EA9055F","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"79f5a55da1045297aa08bcdd708b4e758fbbd21e","datavalue":{"value":"Q127592956","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1577484$E24588DD-BDD8-4A13-9E60-78A0DC5939DF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c4c672886c9edf0b4e96451485a497181af72863","datavalue":{"value":{"entity-type":"item","numeric-id":4281685,"id":"Q4281685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70eedd7d01f0e9392c8231c1a6a73bf195829967","datavalue":{"value":{"amount":"+0.8130788207054138","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":"Q1577484$EFEB6A26-6F86-4DE2-A4A4-93FF865A0C0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d774b848aec03fbaa972ca7064d768c2b50c6b3","datavalue":{"value":{"entity-type":"item","numeric-id":2751377,"id":"Q2751377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a80a654cf2b90e7415f7086becf22234b030a1b7","datavalue":{"value":{"amount":"+0.787391722202301","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":"Q1577484$7C263B59-8B26-4071-AA92-E0E697126C9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2398eef9efd57113e53ce4e1c6dc78ad09f83c74","datavalue":{"value":{"entity-type":"item","numeric-id":4942004,"id":"Q4942004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7354cc2b6bbef02f747da4ea3b09c0a69f5ed79b","datavalue":{"value":{"amount":"+0.7609850764274597","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":"Q1577484$72E6E720-AD0B-4924-A8FF-FCD6F37D64F2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Deciding the \\(E^+\\)-class by an a posteriori, liftable order","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Deciding_the_%5C(E%5E%2B%5C)-class_by_an_a_posteriori,_liftable_order"}}}}}