Calculi in which derivability is decidable by finite interpretations (Q1121677)

A regular Horn system (RH-system for short) is specified by a finite collection of derivation rules \(t_ 1,...,t_ k\to t\), where all \(t_ i\) are of the form q(x) q being an unary predicate symbol, x being a variable, and t is either a term or an unary predicate such that every variable occurs at most once in t. The set of variable-free terms derivable in an RH-system is called the language generated by this system. A finite T-automaton is a quadruple \(A=<V,Q,\psi,D>\), where V is a finite set of function symbols, Q is a finite set of states (the interpretation domain), \(\psi\) maps V to functions over Q and \(D\subseteq Q\) is the set of accepted states. Given a variable-free term, a T-automaton computes its value under the interpretation \(\psi\) and accepts iff this value belongs to D. The following facts are claimed in the paper (some of them are proven, for some only proof hints are given). 1) The class of languages accepted by finite T-automata coincides with the class of languages generated by RH-systems. In this sense derivability in RH-systems is decidable by finite interpretations (in linear time). 2) The class of languages generated by RH-systems is closed under set-theoretic operations. 3) The problems of equality, inclusion, emptiness for the languages generated by RH-systems (accepted by finite T-automata) are decidable. In logical terms, derivability of assertions of the form \(q_ 1(t_ 1)\) \& \(q_ 2(t_ 2)\), \(q_ 1(t_ 1)\vee q_ 2(t_ 2)\), \(q_ 1(t_ 1)\to q_ 2(t_ 2)\), etc. is decidable for RH-systems. 4) A set L of variable-free terms constitute a language generated by an RH-system iff the characteristic relation \(R_ L\) (the maximal congruence relation compatible with L) has a finite number of equivalence classes. 5) The languages generated by RH-systems are closed relative to inverse homomorphisms.