ADC method of proof search for intuitionistic propositional natural deduction.

The ADC method of proof search in propositional natural deduction proposed in 2000 proceeds bottom up first by Analysing the sequent into sub-goals by applying all possible introduction rules, and then by checking whether each of these sub-goals can be established using only elimination rules (Direct Chaining). This looks simpler than the worst case complexity (PSPACE) of the derivability problem for intuitionistic propositional logic.We investigate the complexity ofADC for various fragments. ADC derivability is polynomially decidable for the &,→-fragment by a generalization of a familiar direct chaining algorithm for Horn formulas. Adding ⋁ leads to a CoNP-complete fragment. A short counterexample in case the goal sequent is not ADC derivable is provided by witnessing all relevant disjunctions. Adding constant ⊥ preserves CoNP completeness. [ABSTRACT FROM AUTHOR]