Many applications in Computer Science require to represent knowledge and to reason with non normal form formulas. However,
most of the advances in tractable reasoning are applied only to CNF formulas. In this paper, we extend tractability to several
classes of non normal formulas which are of high practical interest. Thus, we first define three non normal Horn-like classes
of formulas F
1 ∧F
2 ∧... ∧F
n where each F
i
is constituted by a disjunction of two optional terms F
i
= NNF
i
- ∨ C
i
+: the first one is in Negation Normal Form (NNF) composed exclusively with negative literals and the second one is a conjunction
of positive propositions. These formulas codify the same problems that the Horn formulas but with significantly, even exponentially,
less propositional symbols. Second, we define sound and refutational complete inference rule sets for each class. Our third
contribution consists in the design of a sound, complete and strictly linear running time algorithm for each class. As a result,
the time required by our linear algorithms running on the defined non normal Horn-like formulas can be exponentially less
than that required by the existing linear Horn-SAT algorithms.