ON OPTIMIZATION OF MONADIC LOGIC PROGRAMS

This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

Submitted: 2025-02-17; Published: 2025-02-17

This work is licensed under Creative Commons Attribution–NonCommercial International License (CC BY-NC 4.0).

Abstract

The article is devoted to the optimization of monadic logic programs and goals (programs and goals, which do not use functional symbols of arity >1 and use only predicate symbols of arity 1). A program P is terminating with respect to a goal G if an SLD-tree of P and G is finite. In general, monadic programs are not terminating. Program and goal transformations are introduced, by which a monadic program P and a variable-free monadic goal G are transformed into P′ and G′, such that P′ is terminating with respect to G′ and P⊨G if and only if P′⊨G′. Note that the transformed program P′ is the same for all goals.