Maximal contractions in Boolean algebras

In the present paper,the concepts of deductive element and maximal contraction are introduced in Boolean algebras,and corresponding theories of consistency and maximal contractions are studied.An algorithm principle is proposed to compute all maximal contractions for a consistent set with respect to its refutation in Boolean algebras.It is pointed out that the quotient algebra of the first-order language with respect to its provable equivalence relation constitutes a Boolean algebra,and hence the computation of R-contractions for closed formulas in first-order languages can be converted into the one in Boolean algebras proposed in this paper.Furthermore,the concept of basic element is introduced in Boolean algebras,which contributes to the definitions of clause and Horn clause transplanted from logic to a special type of Boolean algebras generated by basic elements.It is also pointed out that the computation of R-contractions for clauses in the classical propositional logic can be converted into the one in Boolean algebras generated by basic elements proposed in this paper.