{"entities":{"Q1198235":{"pageid":1208984,"ns":120,"title":"Item:Q1198235","lastrevid":67075155,"modified":"2026-04-12T14:54:47Z","type":"item","id":"Q1198235","labels":{"en":{"language":"en","value":"A method for simultaneous search for refutations and models by equational constraint solving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 92587"}},"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":"Q1198235$CF961146-CB91-4FFC-9D0F-2755BD24FA9F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1801d6517507c5689a5cee3cdae370a7b20f9dd2","datavalue":{"value":{"text":"A method for simultaneous search for refutations and models by equational constraint solving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1198235$4BE97FA0-4BB1-4C6A-B33C-695565A6DDF9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6cfe5c7be384003c109146e8ed8a094286e8291d","datavalue":{"value":"0770.68104","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1198235$66F566A6-ABA0-4EF0-816C-3E9F38225FCE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d13afdb7bbaba161e87d4a8ab531205253216acb","datavalue":{"value":"10.1016/S0747-7171(10)80014-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1198235$FF2AD5D1-599A-4B08-9743-045542D550C4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef8d9904a40baa08e6f0a10240e7a4f7764dfa82","datavalue":{"value":{"entity-type":"item","numeric-id":167062,"id":"Q167062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$04AAEC71-61C3-45B0-BCE3-E299F599F5FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"de61a30031ada83def5fe35c26b2a988eda26b2b","datavalue":{"value":{"entity-type":"item","numeric-id":1198234,"id":"Q1198234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$1670F8C8-42A0-4543-9CF9-A1B5F7A881D0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$73B634A1-5310-43D0-8A37-095C220A4D09","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"be1a65edbb43ce1fc59464f99e70afbd93e8e2a0","datavalue":{"value":{"time":"+1993-01-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1198235$7A33A31A-CF2A-49D2-B79F-3F831C327C24","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8ba43ca6f99344794d98af7a1a9c93c7d45b8fd4","datavalue":{"value":"A method for simultaneous search for refutations and Herbrand models is proposed. This problem is very interesting when the resolution procedure is used as a decision algorithm and when it is necessary to build a model for a satisfiable formula. New inference rules are proposed which are used in addition to a resolution rule. These new rules use distautology, dissubsumption, disresolution conditions which are formulated as formulas consisting of equalities and inequalities of terms. Introducing new rules it is possible to construct a resolution based decision algorithm for some classes of first order logic e.g. for the Bernays-Sch\u00f6nfinkel class for which no resolution methods is known to be a decision procedure.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1198235$11FE3304-428A-443E-ADBE-D34C243F7EB5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1198235$5375DF5F-33D2-4832-8B93-53F6F6467606","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8c50ce6075a0873a36bf623ea9df073cec5bd171","datavalue":{"value":"92587","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1198235$05450022-E0D2-4CC0-982F-A117ECBF3451","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1198235$F1F556FE-C02B-4CB0-9368-39C2C0AC8D15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d649755d7dec7fe8dd2722580b18ccd4bdd91b89","datavalue":{"value":"equational theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1198235$5542985B-3B2F-49DD-AA26-0C2A0243BF6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1198235$61E04AAB-96F7-4FA5-AFD0-CE33055774D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q1198235$46ACF8FA-5CB9-4114-B42F-F7CB6DCAE1B3","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":"Q1198235$36FC94FC-ABFF-4757-8AD7-2ED20487AC75","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":"Q1198235$3AC8234E-A059-462E-BDDE-30B68789688F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"97f2b2673bf036beb0708e9a25319f486f5c7cd8","datavalue":{"value":{"entity-type":"item","numeric-id":2651970,"id":"Q2651970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$BAC32FA6-B2A4-4329-ABF3-1D4969AABF2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f70484bd2d56db595fa191ad0d54a382774ee3","datavalue":{"value":{"entity-type":"item","numeric-id":3335722,"id":"Q3335722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$67AF3D97-F7F9-4761-8138-3D8FF9030024","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19a2f042bce831ceb861d6edacfa33cb83e3369f","datavalue":{"value":{"entity-type":"item","numeric-id":3818292,"id":"Q3818292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$5E89C840-1988-4CBA-BA3C-B3CF96268DFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f32e4534e98803de8922a9c5dd9e19f52f32d74a","datavalue":{"value":{"entity-type":"item","numeric-id":4279075,"id":"Q4279075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$6F7B97D1-C359-4032-8CE3-C2B74BB8ED60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7251eb542cf9f4bc5047c5105a2dcf8298435daf","datavalue":{"value":{"entity-type":"item","numeric-id":4287493,"id":"Q4287493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$2C67F756-26A4-4580-A023-C9C9ECF3DB33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0285c907a8b1aec6e16d4e2ecf8f1e6d1cb0953","datavalue":{"value":{"entity-type":"item","numeric-id":4038726,"id":"Q4038726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$AE2A20BF-C45B-48A8-85F9-03C71022873C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f241207bb39341afad681685e7fc2b817c7ff774","datavalue":{"value":{"entity-type":"item","numeric-id":1124372,"id":"Q1124372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$DE5A87D7-06A4-44FD-9412-ED8E38D2756D","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":"Q1198235$9D0F6C1F-3DE5-457C-B017-1710B27C3491","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf1eb0085816c68ff7078182501fe6b0337105","datavalue":{"value":{"entity-type":"item","numeric-id":3743300,"id":"Q3743300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$8A0F46F2-0798-4051-9ECF-C7A84FE8865E","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":"Q1198235$2E713D8D-F3BF-47EC-90CF-E28ACEEA51B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eafd1eb7cfc9c85a5ed540ab8f6356e006aaa99f","datavalue":{"value":{"entity-type":"item","numeric-id":1186697,"id":"Q1186697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$2376A033-8F32-4D79-96E9-B2D04FB22397","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c527e263525faa34ac4a72501bf8563b41ad015a","datavalue":{"value":{"entity-type":"item","numeric-id":4297316,"id":"Q4297316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$14231D7B-6F87-4DCF-99C6-1A1488D3D452","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$36E90BA5-A22D-46D1-B2B9-8802EE78D832","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4dfb9c15eb8582237fb4b4fbea1ff81538e5bf8f","datavalue":{"value":{"entity-type":"item","numeric-id":3216155,"id":"Q3216155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$0559F010-A658-4CC8-B171-9B5CD4608B7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5587664e371fa7cdb52e3b1329f22cf9fcff022","datavalue":{"value":{"entity-type":"item","numeric-id":1101242,"id":"Q1101242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$02AD602B-6443-4A6C-A0B6-4DD23D81B5C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"edc6b5f087fec6d157af216327e534fa3b171462","datavalue":{"value":{"entity-type":"item","numeric-id":1148892,"id":"Q1148892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$5AC3ABA0-62C4-4B6D-B18E-D78080E58A7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f771f551f48b2f2d21f6f2011008cb21eb26e492","datavalue":{"value":{"entity-type":"item","numeric-id":5538933,"id":"Q5538933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$F9E7A74B-5C56-44BD-9CD5-4D8042852D10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27ee3b057142576093bd9e66364057980fafc0e4","datavalue":{"value":{"entity-type":"item","numeric-id":1821564,"id":"Q1821564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$607EFAB9-6F3D-4A43-B6EC-F1BDFC5474B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d9c3982efd0f7ccc059068ad9e9a439bba5bf60","datavalue":{"value":{"entity-type":"item","numeric-id":3949989,"id":"Q3949989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$B5D822DB-4022-43D9-9F9D-4AB415332159","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a0f0b2b67b69fedc8c9743c73e818943a9359cf","datavalue":{"value":{"entity-type":"item","numeric-id":3939273,"id":"Q3939273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$D1C62A80-3A4D-4E4F-AB99-2ABBF68DF50B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0620e875ace4454552471ddc26f3c19b333694a","datavalue":{"value":{"entity-type":"item","numeric-id":3994754,"id":"Q3994754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$5DBB8D23-181D-4B46-AE67-C743AF258943","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4724efffc850daf4754d455de6e91abef1b13210","datavalue":{"value":{"entity-type":"item","numeric-id":3681966,"id":"Q3681966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$2CC49861-53CC-4606-955C-935A6DDB5D08","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":"Q1198235$603E359D-B214-45C4-81C7-5EB3EC9584AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6638da077510d95046546294081de23a7659270","datavalue":{"value":{"entity-type":"item","numeric-id":6488530,"id":"Q6488530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1198235$2E94AD82-F116-420C-BC2A-FEC8FA8A5A3A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b218c4ba3c0ee3527ebaf03168166dd2cb9217ec","datavalue":{"value":{"entity-type":"item","numeric-id":4287493,"id":"Q4287493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3868e21703ce40da865088df95b043960ba8b087","datavalue":{"value":{"amount":"+0.8622670769691467","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":"Q1198235$32EADB00-112A-4FA6-86BA-82D02BC72677","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2f395577fbcc727f3706479ec8892d242b633f6","datavalue":{"value":{"entity-type":"item","numeric-id":3348885,"id":"Q3348885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3868e21703ce40da865088df95b043960ba8b087","datavalue":{"value":{"amount":"+0.8622670769691467","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":"Q1198235$1188B967-21FC-42B5-B975-ED8678419F54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d722f8f40862bf2bef4161b78b32e2449d83c4af","datavalue":{"value":{"entity-type":"item","numeric-id":4272502,"id":"Q4272502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0be21fe303683523cc6a03dd643dad6678bcbf01","datavalue":{"value":{"amount":"+0.828224241733551","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":"Q1198235$5B672760-021D-44DA-B3AF-7CC8C52CBCD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44469c695c7d19631de7e636f5e7f496493f9406","datavalue":{"value":{"entity-type":"item","numeric-id":4283235,"id":"Q4283235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51f57c22ee82ee175581415ddf4d0b52923a9cc0","datavalue":{"value":{"amount":"+0.8270640969276428","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":"Q1198235$DC91B956-006F-4171-8300-89C58331EAB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b01627bb4302973460575a627d130f071ccaa00d","datavalue":{"value":{"entity-type":"item","numeric-id":4530458,"id":"Q4530458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"733137a74860a8fdd1541b9ae1fe369f8efbd798","datavalue":{"value":{"amount":"+0.7955403327941895","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":"Q1198235$28ADB8F2-0287-4DF9-A88E-44C8F408A258","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A method for simultaneous search for refutations and models by equational constraint solving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_method_for_simultaneous_search_for_refutations_and_models_by_equational_constraint_solving"}}}}}