Logic programming and automated reasoning. International conference, LPAR `92, St. Peterburg, Russia, July 15--20, 1992. Proceedings (Q1294673)

The articles of mathematical interest will be reviewed individually. The 5th conference 1994 (see Zbl 0875.00092) and the 4th conference 1993 (see Zbl 0875.00121) have been announced. Indexed articles: \textit{Harland, J. A.; Pym, D. J.}, On resolution in fragments of classical linear logic, 30-41 [Zbl 0920.03017] \textit{Galmiche, Didier; Perrier, Guy}, A procedure for automatic proof nets construction, 42-53 [Zbl 0920.03015] \textit{Baaz, Matthias; Fermüller, Christian G.}, Resolution for many-valued logics, 107-118 [Zbl 0920.03019] \textit{Baumgartner, Peter}, An ordered theory resolution calculus, 119-130 [Zbl 0920.03016] \textit{McCune, William; Wos, Larry}, Application of automated deduction to the search for single axioms for exponent groups, 131-136 [Zbl 0925.20002] \textit{Egly, Uwe}, Shortening proofs by quantifier introduction, 148-159 [Zbl 0920.03020] \textit{Parigot, Michel}, \(\lambda\mu\)-calculus: an algorithmic interpretation of classical natural deduction, 190-201 [Zbl 0925.03092] \textit{Boy de la Tour, Thierry; Kreitz, Christoph}, Building proofs by analogy via the Curry-Howard isomorphism, 202-213 [Zbl 0925.68400] \textit{Baker, S.; Ireland, A.; Smaill, A.}, On the use of the constructive omega-rule within automated deduction, 214-225 [Zbl 0920.03018] \textit{Ringeissen, Christophe}, Unification in a combination of equational theories with shared constants and its application to primal algebras, 261-272 [Zbl 0920.08001] \textit{Bachmair, Leo; Ganzinger, Harald}, Nonclausal resolution and superposition with selection and redundancy criteria, 273-284 [Zbl 0925.03063] \textit{Gramlich, Berndhard}, Relating innermost, weak, uniform and modular termination of term rewriting systems, 285-296 [Zbl 0925.68269] \textit{Bai, Mino; Blair, Howard A.}, General model-theoretic semantics for higher-order Horn logic programming, 320-331 [Zbl 0925.68100] \textit{Walther, Christoph}, Computing induction axioms, 381-392 [Zbl 0925.03053] \textit{Salzer, Gernot}, The unification of infinite sets of terms and its applications, 409-420 [Zbl 0925.03071] \textit{Kohlhase, Michael}, Unification in order-sorted type theory, 421-432 [Zbl 0925.03080] \textit{Sattler-Klein, Andrea}, Infinite, canonical string rewriting systems generated by completion, 433-444 [Zbl 0925.68265]