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.
No institution available
Mathematics
, 2025, Issue 1, pp. 1–10
ISSN Online: 0000-0000
DOI:
10.xxxx/example-doi