{"entities":{"Q1333268":{"pageid":1344007,"ns":120,"title":"Item:Q1333268","lastrevid":68491092,"modified":"2026-04-13T00:03:35Z","type":"item","id":"Q1333268","labels":{"en":{"language":"en","value":"Equational formulae with membership constraints"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 638560"}},"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":"Q1333268$74ABDE57-EDB7-423A-818E-60E4F25290F0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f3b7383c5ea2ed278236c345cc27b1284b7cb7b4","datavalue":{"value":{"text":"Equational formulae with membership constraints","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1333268$3EBD0357-7257-4A73-9D8E-201B218FBC7A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d73a87a92a1234c42ada92c6f00560b2cc13a18d","datavalue":{"value":"0827.03020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$B81A16E8-FF1D-4ADC-BF31-016AAC3C136E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"23be70569faa30ab86ceaac20a2ea57705fd5fb4","datavalue":{"value":{"entity-type":"item","numeric-id":685392,"id":"Q685392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1333268$DFC69142-9B5C-428E-A737-60A621CD471F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eca38b7143b5cec712c284a60afe6cf1b805a7cb","datavalue":{"value":{"entity-type":"item","numeric-id":1333267,"id":"Q1333267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1333268$4DCABA03-148E-41C8-A939-9197389AC3C8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1333268$0B54BD1E-1750-4065-A343-0E53B8EDA337","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d2c5a0478135439b51e1336eb30896ff68f823dd","datavalue":{"value":{"time":"+1995-12-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1333268$7844490C-B15C-4D76-9AA9-3507DB54E8DF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"15e134c6982ba0d5ffa5a31cb63edecec288c326","datavalue":{"value":"The ``automated'' transformation of equational formulae into ``simpler'' forms has many applications (functional and logic programming; abstract data types; automated deduction, a.s.o.). The formal framework is given by equational formulae in order-sorted algebras. The equational formulae are here first-order logical formulae whose atoms are either equations (\\(t=s\\), where \\(t\\) and \\(s\\) are terms over an order-sorted signature), or membership constraints (\\(t\\in \\tau\\), where \\(t\\) is a term and \\(\\tau\\) is a sort). A solved-form of an equational formula represents either \\(\\perp\\) (meaning ``no solution'') or a most general unifier (a solution of the considered formula), having the same syntactical form. In the chosen context, solvability is decidable and a correct set of transformation (rewriting) rules is provided. ``The main results are termination and completeness of our set of rules''. Quantifier elimination is also treated. The last part of the paper is devoted to the study of some applications and consequences (such as the axiomatization of a structure describing a regular tree language, or automatic proofs by induction in equational theories). A preliminary version by the first author of this work appeared in the Proceedings of the ICALP 1990, under the title ``Equational formulas in order-sorted algebras'' [Lect. Notes Comput. Sci. 443, 674-688 (1990; Zbl 0774.68071)].","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$C6440BDB-95B1-45EF-8EE3-AA75BFFC0BC6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed4ac44229a63771ae4ded31038fe93f434bffb7","datavalue":{"value":"03C05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$DB49F1C1-F63C-4990-85E6-76D730E81F69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"176e47af9f9e7cf4ebff07fc1f9e4f94a83134c1","datavalue":{"value":"03C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$799551D6-9885-40EF-AB81-767E947DE518","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$C47E3C66-A367-442A-85D9-7E42A4F8D3B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$D0A3E985-A0EE-49A6-B380-E61016AB5B82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$45C258DD-19B8-4C48-A0C8-5C8F7BF8833C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"70965dc9a0b1686bb84c003f7f4b614e78798461","datavalue":{"value":"638560","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$7D023B68-71A9-4FED-8EE1-B466586C825A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb212c449f11e0594f2ac60cfd20e7a5e1b5c40e","datavalue":{"value":"equational formulae","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$CD5F2880-E9F5-4867-997C-0C099F72CCFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb40407ee82a936477220c4442becd1f17199ff2","datavalue":{"value":"order-sorted algebras","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$DC57EB67-D9FB-432E-A76A-9742BCBD89DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ac16a21d51e0878fa32c336d0abd8733faecc47","datavalue":{"value":"membership constraints","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$CB974C70-D613-4516-9BD5-B075F7AEF495","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51652e8c51d0740ad2999d6a8e9c64e45e13e225","datavalue":{"value":"unifier","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$0CD2FAFA-7A5A-48E5-B6F8-79A917513448","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d08be6f7ad8da62ec6e1cfb385e8cc060cd14529","datavalue":{"value":"solvability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$9254187E-1B09-4CC9-BC34-A80E04257832","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c4978f2c4d263ef258ed0ffc576a325d510c4d8","datavalue":{"value":"axiomatization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$0773A60E-DCB2-47F3-8138-6C63D21EBC47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ed418a28386cecb26257f7dc60b7ef2091286d8f","datavalue":{"value":"regular tree language","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$99B4F031-43C7-41A3-8AB1-CFD804B72DBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61625fed2f2d49375162a528dbcacee2d500d495","datavalue":{"value":"automatic proofs by induction in equational theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1333268$DDE76D61-0E10-46B3-B129-7C0F5554F77A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"6536f759dee9ce142c834adc5cc137400d919eb8","datavalue":{"value":{"entity-type":"item","numeric-id":1037240,"id":"Q1037240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1333268$4BB2C472-6EEF-453F-ACB4-92637E4583D1","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":"Q1333268$91F18941-195F-4EF7-A97C-D3CF201BDDFF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b2d7e733fa3d91aea41b170caf676d6c13e371ad","datavalue":{"value":"https://doi.org/10.1006/inco.1994.1056","type":"string"},"datatype":"url"},"type":"statement","id":"Q1333268$935B9547-0608-42B0-8974-EF414928E380","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f7d2570d37f39a428e81d65d6b6ccdda4369cd49","datavalue":{"value":"W1964783683","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$E27AE3EC-C71F-4839-A797-5FC3BFA34F52","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c39e2602d41ea5ec61e251102ccef8358f92f369","datavalue":{"value":"10.1006/INCO.1994.1056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1333268$8A64C7A6-45BB-4C8C-8A41-D5DD6634C63D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"93ad6aa4d340344d58f34be706e4f8741bb2f4e9","datavalue":{"value":{"entity-type":"item","numeric-id":4038726,"id":"Q4038726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"857e2191e0cf35e7b034bd56e25a4993d900ca5d","datavalue":{"value":{"amount":"+0.89151335","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$F9AEDF25-487B-4DEF-85EC-2CAD160A3161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af0f3477d5e3449868257bdbb549b0f0584ca70b","datavalue":{"value":{"entity-type":"item","numeric-id":1264438,"id":"Q1264438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e25200dfdb01cc1f689a0dc2af3dab41ea2aa946","datavalue":{"value":{"amount":"+0.83354706","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$C50CE2E1-717B-4A6C-A42D-1356FF72AD41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc5eb68999c3412297b5ef52f0fb23f5595c190c","datavalue":{"value":{"entity-type":"item","numeric-id":3804236,"id":"Q3804236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c733b3819394828470432c0cc779be646d600bc","datavalue":{"value":{"amount":"+0.830966","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$CA4B16A7-CEA8-4309-81C3-C164B241BDEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af6729f1ba184281871f04967d8eace73e2b9b3f","datavalue":{"value":{"entity-type":"item","numeric-id":3792234,"id":"Q3792234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"906e64449142f0882ae2daa8966ddf12d4528f53","datavalue":{"value":{"amount":"+0.83004856","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$732ECDAB-5BAC-4906-9F6B-19987862A336","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5bd0fa66fd9009baaa2529908f98e3f28360a72","datavalue":{"value":{"entity-type":"item","numeric-id":5055713,"id":"Q5055713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"efa2e81da8fac7ef6122ddaa45788b35ebc22858","datavalue":{"value":{"amount":"+0.8300169","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$40469629-F239-4759-A6B3-A9978055B82F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87931669e1651228992cdbf1bcc05dfc01c8ee4e","datavalue":{"value":{"entity-type":"item","numeric-id":1124372,"id":"Q1124372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12825132103ba6237fabc89eb3039c30aa7df2b5","datavalue":{"value":{"amount":"+0.82854724","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$40B6B428-73B0-48C0-8627-B8C89CD46B37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e833c8a27f9027a689f51b813a46229e5590e5d1","datavalue":{"value":{"entity-type":"item","numeric-id":6486039,"id":"Q6486039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed39caa1752271905c3094dc744524e570b32774","datavalue":{"value":{"amount":"+0.8268235","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$D953C1F4-9BBC-44F1-B3A5-7D77297AFFBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04b88390e1984f0b3f5227ed4240b40a6b764274","datavalue":{"value":{"entity-type":"item","numeric-id":5204334,"id":"Q5204334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30f52830c614ead9510c4a1602c05bf411e6db24","datavalue":{"value":{"amount":"+0.8220532","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$2B6E7BA4-F0D1-405A-A292-6F78C6E3CCA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5bf0f16f9bd2a779f2f0fde3110857be40584aed","datavalue":{"value":{"entity-type":"item","numeric-id":1322836,"id":"Q1322836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1a15351eaab1e30076ffa47d21ca7ba06b955b8","datavalue":{"value":{"amount":"+0.81864125","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$5A425F16-9F71-45F2-B20D-991D7186EBEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c0ac43329cb5bdfaa9b1979e611afebb0a9b34c0","datavalue":{"value":{"entity-type":"item","numeric-id":3696486,"id":"Q3696486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed89ac43b024eede083fbfb6d11a9199a3c09b12","datavalue":{"value":{"amount":"+0.81709254","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1333268$4AEF3352-C059-45DD-B626-EB989AE4B0CD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Equational formulae with membership constraints","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Equational_formulae_with_membership_constraints"}}}}}