Incremental Version of the Modern Syllogistic Method

An algorithmic technique for truth-preserving deduction in propositional logic is the Modern Syllogistic Method (MSM). This method casts a set of premises into a single switching function equated to zero, and then obtains the complete sum of this function as a disjunction of all prime consequents. An incremental version of the MSM augments the original set of premises by new ones, and seeks the updated consequences incrementally, i.e., without having to recalculate the complete sum from scratch. This paper presents a novel enhanced form of Blake-Tison method for computing the complete sum of a switching function, and explains how to use it efficiently in an incremental MSM. The method is illustrated with four demonstrative examples with particular attention to the issues of inconsistency, selective deduction, optimal order of variables, and single-literal premises.