20
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: not found
      • Article: not found

      A compact representation of proofs

      Studia Logica
      Springer Nature

      Read this article at

      ScienceOpenPublisher
      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Related collections

          Most cited references7

          • Record: found
          • Abstract: found
          • Article: not found

          A formulation of the simple theory of types

          The purpose of the present paper is to give a formulation of the simple theory of types which incorporates certain features of the calculus of λ-conversion. A complete incorporation of the calculus of λ-conversion into the theory of types is impossible if we require that λx and juxtaposition shall retain their respective meanings as an abstraction operator and as denoting the application of function to argument. But the present partial incorporation has certain advantages from the point of view of type theory and is offered as being of interest on this basis (whatever may be thought of the finally satisfactory character of the theory of types as a foundation for logic and mathematics).
            Bookmark
            • Record: found
            • Abstract: found
            • Article: not found

            Linear reasoning. A new form of the Herbrand-Gentzen theorem

            In Herbrand's Theorem [2] or Gentzen's Extended Hauptsatz [1], a certain relationship is asserted to hold between the structures of A and A′, whenever A implies A′ (i.e., A ⊃ A′ is valid) and moreover A is a conjunction and A′ an alternation of first-order formulas in prenex normal form. Unfortunately, the relationship is described in a roundabout way, by relating A and A′ to a quantifier-free tautology. One purpose of this paper is to provide a description which in certain respects is more direct. Roughly speaking, ascent to A ⊃ A′ from a quantifier-free level will be replaced by movement from A to A′ on the quantificational level. Each movement will be closely related to the ascent it replaces.
              Bookmark
              • Record: found
              • Abstract: found
              • Article: not found

              Resolution in type theory

              In [8] J. A. Robinson introduced a complete refutation procedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand's Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many statements of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinction between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.).
                Bookmark

                Author and article information

                Journal
                Studia Logica
                Stud Logica
                Springer Nature
                0039-3215
                1572-8730
                December 1987
                December 1987
                : 46
                : 4
                : 347-370
                Article
                10.1007/BF00370646
                6e233369-0c59-4b4a-acf6-e41621702d33
                © 1987
                History

                Comments

                Comment on this article