{"entities":{"Q1060023":{"pageid":1061871,"ns":120,"title":"Item:Q1060023","lastrevid":66056487,"modified":"2026-04-12T07:14:45Z","type":"item","id":"Q1060023","labels":{"en":{"language":"en","value":"Verifying the unification algorithm in LCF"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3905873"}},"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":"Q1060023$B9440046-8F20-40FE-A60A-4C3CCF089DDD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"06a1ce71ac95bb63892517ea49472bda9b8caf40","datavalue":{"value":{"text":"Verifying the unification algorithm in LCF","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1060023$B450A3A2-AF4E-4BDA-A6B8-8F07BA614F2E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c1e3bea2756a243b0111c8bbef9a5f7808074a38","datavalue":{"value":"0567.68054","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060023$5E34453E-7376-4FE9-8004-3B14E012E700","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"faeb8d56d25b54cfef7cbae86200ef8b1f6eaf9b","datavalue":{"value":"10.1016/0167-6423(85)90009-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060023$0C5D9095-1CFE-42F7-9CE9-F71C55CF357B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060023$B9C0CBD8-D6BF-48ED-81F5-446EFE6C1F30","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3c94df5c9af0ede578c52141befd29044de13172","datavalue":{"value":{"time":"+1985-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":"Q1060023$0C424F85-56DD-4908-87AF-339B84057BE2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"82efcf412e4cc32be503a05136bd0126dbe999c6","datavalue":{"value":"\\textit{Z. Manna} and \\textit{R. Waldinger}'s [ibid. 1, 5-48 (1981; Zbl 0472.68054)] theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitution is presented as a detailed example of interaction with LCF. Translating the theory into LCF's domain-theoretic logic is largely straightforward. Correctness of unification is expressed using predicates for such properties as idempotence and most-generality. Well-founded induction on a complex ordering is translated into nested structural inductions. The inductions divide the verification into lemmas: a constant is unifiable with itself, a constant is not unifiable with a combination, etc. The LCF proofs are compared with the original ones. Most of the work is devoted to proving that unification terminates. LCF's approach to termination proofs is compared with that of Boyer and Moore and others.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060023$F13D71E4-6E86-448C-ACA0-291BC2A19816","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060023$C59296DD-AEF9-42A1-AC57-E4E35EC6A476","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060023$B80959E7-AFD6-4F01-B4E6-4C4750F77FB2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"46e325fadbb309aa8911cc4dc7d27a626fe26ead","datavalue":{"value":"3905873","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060023$27D9C86D-17EB-46A7-995A-0A62401318AC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab83b74f8204ae5e13a88c27dae843296e492dc0","datavalue":{"value":"substitutions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060023$BF59FAE7-B724-4143-AB6B-EA18BA688AE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cdb582a6e197d9561cf7fbd2aebdeeb4ddba8d7c","datavalue":{"value":"Cambridge LCF theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060023$23DD4905-5907-42C9-9385-46DEE2B06898","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4befa4ca20f2beabcfa09e8a92ae13c21cb4934a","datavalue":{"value":"termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1060023$D95BC346-0C7D-4B1B-AF33-A64ED540DE4D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"9991ec1659040b5b234de05231b2049af8d2b873","datavalue":{"value":"Q57382754","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060023$8B83C7D4-D9CA-42F5-862A-275FB8DC33C2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060023$6A2F16B3-603A-4D24-A773-0FFDC6FE4490","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060023$535DC58E-B0C5-4AA5-A3BD-0580051E8AFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1060023$810A9671-89C5-4203-9CDD-6197A2BF4ED0","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":"Q1060023$5F6D818F-E6CF-4B73-927F-2234B048B2DF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cab58ad659bb854406f946fbd4a1bb8a817a8871","datavalue":{"value":"https://doi.org/10.1016/0167-6423(85)90009-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q1060023$B602CE41-B1DC-4CEC-B4B7-0901226B3B2F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9c58d2b6b092591e4fde7e5a31420f2f4c39f1dc","datavalue":{"value":"W2019994514","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1060023$0604D5D0-82E0-4CD8-AF3A-396C3154DE3A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b31b77fca7c9b8ba84a5adfb7106757a93e764bb","datavalue":{"value":{"entity-type":"item","numeric-id":3696549,"id":"Q3696549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1682729e86d134cb67c383dca5a9589bbe49b99","datavalue":{"value":{"amount":"+0.7753334045410156","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":"Q1060023$B216E14B-CE29-4851-9786-9AECD590C313","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94270c777b69360d62a77ecf64e4992a560b5e61","datavalue":{"value":{"entity-type":"item","numeric-id":4931594,"id":"Q4931594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a7ae0d93c2eaf4c82dc472477472c7d3489a7dc5","datavalue":{"value":{"amount":"+0.7744587659835815","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":"Q1060023$C0C6C523-3E97-4B62-8C8B-C6A4074384CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1be56a5e540eb2a386bedc5e403d6cf01ab17e69","datavalue":{"value":{"entity-type":"item","numeric-id":3160301,"id":"Q3160301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dd92a0ba11a7d62ea13cb5c3efeb8338520bdb0","datavalue":{"value":{"amount":"+0.7715921401977539","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":"Q1060023$9D99162E-5C41-4F34-A706-6AA8D3F3B015","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bbb483c2684f4627d50245224e740d066f55a422","datavalue":{"value":{"entity-type":"item","numeric-id":3326880,"id":"Q3326880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea18e6a0e42f98604652f4fd862acb9c39b1252b","datavalue":{"value":{"amount":"+0.7655080556869507","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":"Q1060023$1FCDDAC9-A7D8-4166-B715-3E3BF38CFA7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d23a7beb7645e5912a00407c2fa6470a87fb5b7","datavalue":{"value":{"entity-type":"item","numeric-id":877825,"id":"Q877825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac74f738ca0fe5c463e5643dd589d5aa89bdde1e","datavalue":{"value":{"amount":"+0.7595760822296143","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":"Q1060023$36B16DA2-ADA0-4ECD-A991-83AAEC2FB344","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verifying the unification algorithm in LCF","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verifying_the_unification_algorithm_in_LCF"}}}}}