Spelling suggestions: "subject:"unification, cycle, equation"" "subject:"reunification, cycle, equation""
1 |
A nice Cycle Rule for Goal-Directed E-unificationMorawska, Barbara 31 May 2022 (has links)
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.
|
Page generated in 0.1319 seconds