Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations

摘要

We present a specialised (polynomial-based) rule for the propositional logic called the Independence Ride, which is useful to compute the conservative retractions of propositional logic theories. In this paper we show the soundness and completeness of the logical calculus based on this rule, as well as other applications. The rule is defined by means of a new kind of operator on propositional formulae. It is based on the boolean derivatives on the polynomial ring F_2[x].