
doi: 10.1007/bf00379762
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.
finite control algorithms, Specification and verification (program logics, model checking, etc.), predicate logic, push-down algorithms, recursive programs, Mechanization of proofs and logical operations, proof searching procedures, Algorithms in computer science, Gentzen type formalizations, iterative programs, propositional logics, Abstract data types; algebraic specification
finite control algorithms, Specification and verification (program logics, model checking, etc.), predicate logic, push-down algorithms, recursive programs, Mechanization of proofs and logical operations, proof searching procedures, Algorithms in computer science, Gentzen type formalizations, iterative programs, propositional logics, Abstract data types; algebraic specification
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
