A modular reduction of regular logic to classical logic

In this paper we first define a reduction δ that transforms an instance Γ of Regular-SAT into a satisfiability equivalent instance Γ^δ of SAT. The reduction δ has interesting properties: (i) the size of Γ^δ is linear in the size of Γ, (ii) δ transforms regular Horn formulas into Horn formulas, and (iii) δ transforms regular 2-CNF formulas into 2-CNF formulas. Second, we describe a new satisfiability algorithm that determines the satisfiability of a regular 2-CNF formula Γ in time O(|Γ|log|Γ|); this algorithm is inspired by the reduction δ. Third, we introduce the concept of renamable-Horn regular CNF formula and define another reduction δ´ that transforms a renamable-Horn instance Γ of Regular-SAT into a renamable-Horn instance Γ^δ´ of SAT. We use this reduction to show that both membership and satisfiability of renamable-Horn regular CNF formulas can be decided in time O(|Γ|log|Γ|)