TR-2003007: On the Complexity of the Reflected Logic of Proofs
Nikolai V. Krupski · CUNY Academic Works (City University of New York) · 2003
Artemov's system LP captures all propositional invariant properties of a proof predicate "x proves y" ([1, 3]).Kuznets in [5] showed that the satisfiability problem for LP belongs to the class Π p 2 of the polynomial hierarchy.No nontrivial lower complexity bound for LP is known.We describe quite expressive syntactical fragment of LP which belongs to N P .It is rLP ∧,∨ -the set of all theorems of LP which are monotone boolean combinations of quasiatomic formulas (facts of sort "t proves F ").A new decision algorithm for this fragment is proposed.It is based on a new simple independent formalization for rLP (the reflected fragment of LP) and involves the corresponding proof search procedure.Essentially rLP contains all the theorems of LP supplied with additional information about their proofs.We show that in many respects rLP is simpler than LP itself.This gives the complexity bound (N P ) for rLP.In addition we prove a suitable variant of the disjunctive property which extends this bound to rLP ∧,∨ .1