PT Book AU Kulaš, M TI A practical view on substitutions SE Informatik-Berichte PY 2016 VL 372 PU FernUniversität in Hagen WP https://ub-deposit.fernuni-hagen.de/receive/mir_mods_00000706 LA en DE substitution; renaming; term matching; generality AB For logic program analysis or formal semantics, the issue of re- naming terms and generally handling substitutions is inevitable. We revisit substitutions from a practitioner’s point of view, pre- senting concepts we found useful in dealing with operational se- mantics of pure Prolog. A concept of relaxed core representation is introduced, upon which a concept of prenaming is built. Prenam- ing formalizes the intuitive practice of renaming terms and allows for extensibility. A novel algorithm for term matching is proposed, which also solves the problem of substitution generality (and thus equivalence), using witness term technique. The technique aleviates the problem of ad-hoc proofs involving generality. PI Hagen ER