Handbook of Automated Reasoning

7.5 The Inverse Method

The inverse method was proposed by Maslov [1964]. Its basic inference rules are formulated in terms of a given set of (generalized) disjunctions of conjunctions of formulas. In our description of the method we follow Lifschitz [1989], where the method is formulated for disjunctions G ₁ ∨ … ∨ G _k of conjunctions G _i =L _i,1∧…∧L _{i,m i} of literals L _i,j . The disjunctions have been called “super-clauses”, and the conjunctions G _i , “super-literals” in [Lifschitz 1989]. The negation ¬G _i of a super-literal, which is equivalent to a standard clause, is denoted by ${\overline{G}}_i$ . Given a set of input super-clauses, ...