In this paper we improve a goal-directed E-unification procedure by introducing a new rule, Cycle, for the case of collapsing equations, i.e. equations of the type x ≈ v where x ∈ Var (v). In the case of these equations some obviously unnecessary infinite paths of inferences were possible, because it was not known if the inference system was still complete if the inferences were not allowed into positions of x in v. Cycle does not allow such inferences and we prove that the system is complete. Hence we prove that as in other approaches, inferences into variable positions in our goal-directed procedure are not needed.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:79317 |
| Date | 31 May 2022 |
| Creators | Morawska, Barbara |
| Publisher | Technische Universität Dresden |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:report, info:eu-repo/semantics/report, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | urn:nbn:de:bsz:14-qucosa2-785040, qucosa:78504 |
Page generated in 0.0022 seconds