Programs and logics (Q1070221)

The paper is concerned with a relationship between programs and Gentzen type formalizations of predicate and propositional logics. It turns out that finite control algorithms (which serve as models of iterative programs) are sufficient for describing the proof searching procedures for propositional logics which admit cut-free Gentzen type formalization, whereas push-down algorithms (which are adequate models for programs with recursive procedures) are needed to describe those procedures for predicate calculi.