{"entities":{"Q1106659":{"pageid":1117408,"ns":120,"title":"Item:Q1106659","lastrevid":69656505,"modified":"2026-04-13T08:30:16Z","type":"item","id":"Q1106659","labels":{"en":{"language":"en","value":"Critical pair criteria for completion"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4062565"}},"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":"Q1106659$1A9E1E21-C7D8-4BFE-B823-D2CD2F6C7180","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"175c6ddbdf8e157473188a91d04ce18ba2e19552","datavalue":{"value":{"text":"Critical pair criteria for completion","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1106659$216131D5-E577-4060-81A7-DE4B3927B981","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7ec4de2c9ab8310715f574c18626d70a46aab87e","datavalue":{"value":"0651.68030","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106659$8FBBFE51-B78B-43E7-8B9A-DB086ED415C2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4fb5e855079af6ada445a3bdd8c85e47a6359980","datavalue":{"value":"10.1016/S0747-7171(88)80018-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106659$31F6739B-586C-4427-946E-A30BA376A7EC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0cf815526c4f2604ee47e98322610a52470dc8b3","datavalue":{"value":{"entity-type":"item","numeric-id":1072370,"id":"Q1072370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$D4F765FE-7220-42BC-A989-25A534A3CB80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"423424ed34b7dac382d00344caf66effb4c7fafb","datavalue":{"value":{"entity-type":"item","numeric-id":199247,"id":"Q199247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$19E67E71-470F-46D9-BD9B-B58D1D56D917","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":"Q1106659$8C320368-21B7-48EA-94EB-0C3909E35365","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1106659$E0925306-A9AF-4F92-9E61-10669153F335","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"361605cec704c98c9fc0632e5c4d0429ffa5bb44","datavalue":{"value":"We formulate the Knuth-Bendix completion method at an abstract level, as an equational inference system, and formalize the notion of critical pair criterion using orderings on equational proofs. We prove the correctness of standard completion and verify all known criteria for completion, including those for which correctness had not been established previously. What distinguishes our approach from others is that our results apply to a large class of completion procedures, not just to a particular version. Proof ordering techniques therefore provide a basis for the design and verification of specific completion procedures (with or without criteria).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106659$DD12F454-6278-4022-88DF-72A49D17CC1B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106659$F6020A24-2A19-4BC6-971F-113713CBECAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106659$47E2026E-039C-4725-9585-6D06570020A7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5ae6bd54061a204082abddb1c4322b6ab2d862b6","datavalue":{"value":"4062565","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1106659$C8C5F4A1-F7D8-439D-9BC1-3DF7E1B673DC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"019a6ed5982241abb5ad173ea9f0389406288f3d","datavalue":{"value":"Knuth-Bendix completion","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106659$BCB041E9-8EAD-4BFB-8F1C-5A7A0801FCBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c4dfe9f5644ad5ddd6f67902b5ba29ab925510e","datavalue":{"value":"equational inference system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106659$B4946BAB-50C5-444E-83C5-FF90E44D5201","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"840232c250b1e1458d71cfdc7fbe467b8d493361","datavalue":{"value":"critical pair","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106659$DD1052C4-3264-4622-80FD-14975096632D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a0d8f70437f98b58f5f0afb7f47b091de88a217c","datavalue":{"value":"orderings on equational proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1106659$BC12E986-09C1-4B6E-B895-EAC7ECC560CC","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":"Q1106659$AD0653EC-4BAE-4867-8B27-ABAD347D4908","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"59bb3344b4f89870291c44462654819d8a7d7295","datavalue":{"value":{"entity-type":"item","numeric-id":3809306,"id":"Q3809306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$E09CD6D4-2093-4C73-AC8F-C2921AA69C2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b7a76e3d93219f8f35922f7e651242be822568a","datavalue":{"value":{"entity-type":"item","numeric-id":3208084,"id":"Q3208084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$254BD49C-E95A-48E0-8EA5-FD0E6CA2FCB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c29888ffc34074a279b8622e0e463f8cf0dd8abd","datavalue":{"value":{"entity-type":"item","numeric-id":3336682,"id":"Q3336682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$5347C705-634E-425D-BF20-B92FD3802AF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ec45a842bd7bf87466a82e7175870b8977fe49b","datavalue":{"value":{"entity-type":"item","numeric-id":3707361,"id":"Q3707361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$14653E63-D292-4C5E-8F8F-0E30123CDC62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b27d44a0e50fda314668a36654efb04ab5135cb3","datavalue":{"value":{"entity-type":"item","numeric-id":3868730,"id":"Q3868730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$D9749CD7-1037-4DF7-88A5-2B773A1FAE15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7814c93fd14c472a24a528c1ff4a97ba1b2c10db","datavalue":{"value":{"entity-type":"item","numeric-id":802317,"id":"Q802317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$45E3A5E2-D98C-4920-B37F-E00B91913F4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"599c5dbf52817fbbe5f2f15e33a96dc6ac97514e","datavalue":{"value":{"entity-type":"item","numeric-id":3908463,"id":"Q3908463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$43602B24-582F-4582-B840-05D8ED62F32A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7dd076536f3668f703f8f8e17b2cfee8106654e","datavalue":{"value":{"entity-type":"item","numeric-id":1154801,"id":"Q1154801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$E3D5D251-BC8F-415D-AE74-6C7E4288FA4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fdeb57f4e5d37efa40bca3185df7185c3f2accb6","datavalue":{"value":{"entity-type":"item","numeric-id":789177,"id":"Q789177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$AA150CFF-F2BF-4D53-BEFE-4DB0CB597833","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"849241baa6b3c56591969b2586e51dae90f667cf","datavalue":{"value":{"entity-type":"item","numeric-id":3816048,"id":"Q3816048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$4FDECA9D-3218-4A4D-9F99-0A0B5DF06731","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$6C44C65B-988A-4432-A846-242C54FB0690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b81bac0c83a1bb3be4d60a72c12b74b133412b10","datavalue":{"value":{"entity-type":"item","numeric-id":3702510,"id":"Q3702510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$29899763-1D48-4C21-B17A-6D70C5D799EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"afa9ce8b4776bea0fbc531870b27f0223a4c6bf6","datavalue":{"value":{"entity-type":"item","numeric-id":3993260,"id":"Q3993260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$F47A946A-ABB8-492F-A620-E5D4CCDC0399","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22c3a2ac2fd98947974c14bdc504e4185a3beff1","datavalue":{"value":{"entity-type":"item","numeric-id":3992832,"id":"Q3992832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$11448B48-0390-4767-BE63-03E3F29E2DA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8670a1cb5138f59a7607a06c6c33e9eef7f2c9ea","datavalue":{"value":{"entity-type":"item","numeric-id":3938536,"id":"Q3938536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$76794125-7392-4995-B1FA-6F81B94BDAA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"031d93ba0f0d59696b935bd9707e0c0dc3b5aa4f","datavalue":{"value":{"entity-type":"item","numeric-id":4050191,"id":"Q4050191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$3BA3C3DE-0B7A-4A46-A59A-DE46E74D4DA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"32ad5aef9d0818bedbf78e0ab4947d22e4e11a42","datavalue":{"value":{"entity-type":"item","numeric-id":3675515,"id":"Q3675515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$6AFCC730-F4C1-4A04-88BD-095F13C766E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0693ec7a4ab1ed4a5c14ca5a8d1f9889cb4a1cba","datavalue":{"value":{"entity-type":"item","numeric-id":3702509,"id":"Q3702509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$6EF5BF79-3BEC-4E0A-8CBF-7DFC51B87100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27e2d761ccb0b052ed932a9e25e1934d9433dace","datavalue":{"value":{"entity-type":"item","numeric-id":3745825,"id":"Q3745825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1106659$38C8AAB5-7AD6-4917-A5AA-F7478C7C2D39","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a38861aa8c5ba98116a45571edd8abc1a857d15","datavalue":{"value":{"entity-type":"item","numeric-id":3993260,"id":"Q3993260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75289e134a0232cf5d1847afc6ad857ba932f933","datavalue":{"value":{"amount":"+0.8882988691329956","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":"Q1106659$8342E1EA-81B1-4F37-BEC1-4E2F181BE3A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d44b80ae72552fe355c6d62c8e6e6500eb145a21","datavalue":{"value":{"entity-type":"item","numeric-id":3806800,"id":"Q3806800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d0a2b303a76fbeb20dc9afbae2267a94fce18a3","datavalue":{"value":{"amount":"+0.8393559455871582","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":"Q1106659$AE2C92DA-1E83-4EA7-8C13-CACF3C537D04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb702b31474b2685d3f88e0ccfb35977d81816b7","datavalue":{"value":{"entity-type":"item","numeric-id":3721811,"id":"Q3721811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9eff075366c205c5430e5162f86ad48874ac7f4","datavalue":{"value":{"amount":"+0.8355935215950012","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":"Q1106659$F1189B1F-6D60-4935-9106-B719F6AEAE38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1aafb895079b756bb43474f20142b29c28337fb0","datavalue":{"value":{"entity-type":"item","numeric-id":5210806,"id":"Q5210806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bb0afcb8e9ac67b5967aaaccf42ed9ab90b77624","datavalue":{"value":{"amount":"+0.8299850225448608","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":"Q1106659$5A645FD4-1833-4549-9DC5-E1E723733FF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9edbafef8ba611e0c51d41d900c2acd1cff7aa43","datavalue":{"value":{"entity-type":"item","numeric-id":3817656,"id":"Q3817656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46f0ea26d526990a8eac92233d4fd12dd7706a31","datavalue":{"value":{"amount":"+0.8245487809181213","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":"Q1106659$4BDF5A13-6616-4A7D-A13D-8AD4BC67C49E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Critical pair criteria for completion","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Critical_pair_criteria_for_completion"}}}}}