## Logic programming and automated reasoning. International conference, LPAR ‘92, St. Peterburg, Russia, July 15–20, 1992. Proceedings.(English)Zbl 0916.00020

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

### MSC:

 00B25 Proceedings of conferences of miscellaneous specific interest 68-06 Proceedings, conferences, collections, etc. pertaining to computer science 03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations 03B35 Mechanization of proofs and logical operations 68N17 Logic programming 68T27 Logic in artificial intelligence

### Citations:

Zbl 0875.00092; Zbl 0875.00121