3. LPAR 1992: St. Petersburg, Russia

Semantics I

• Halina Przymusinska, Teodor C. Przymusinski, Hirohisa Seki:
  Soundness and Completeness of Partial Deductions for Well-Founded Semantics. 1-12
  

Non-Resolution Theorem Proving I

• Steffen Hölldobler:
  On Deductive Planning and the Frame Problem. 13-29
  
• James Harland, David J. Pym:
  On Resolution in Fragments of Classical Linear Logic. 30-41
  
• Didier Galmiche, Guy Perrier:
  A Procedure for Automatic Proof Nets Construction. 42-53
  

Constraints

• James Bowen, Dennis Bahler:
  Free Logic and Infinite Constraint Networks. 54-65
  

Data Bases and Knowledge Bases

• Beat Wüthrich:
  Towards Probabilistic Knowledge Bases. 66-77
  
• Barrett R. Bryant, Aiqin Pan:
  Two-Level Grammar: A Funtional/Logic Query Language for Database and Knowledge-Base Systems. 78-83
  
• Burkhard Freitag:
  Extending Deductive Database Languages by Embedded Implications. 84-95
  

Resolution Theorem Proving

• Ewing L. Lusk:
  Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years. 96-106
  
• Matthias Baaz, Christian G. Fermüller:
  Resolution for Many-Valued Logics. 107-118
  
• Peter Baumgartner:
  An Order Theory Resolution Calculus. 119-130
  
• William McCune, Larry Wos:
  Application of Automated Deduction to the Search for Single Axioms for Exponent Groups. 131-136
  

Theorem Proving and Complexity

• Hai-Ping Ko, Mark E. Nadel:
  Elementary Lower Bounds for th Length of Refutations. 137-147
  
• Uwe Egly:
  Shortening Proofs by Quantifier Introduction. 148-159
  

Implementation Aspects

• Håkan Millroth:
  Reform Compilation for Nonlinear Recursion. 160-171
  
• Ulrich Neumerkel:
  Pruning Infinite Failure Branches in Programs with Occur-Check. 172-177
  

Logical Frameworks

• Andrew Ireland:
  The Use of Planning Critics in Mechanizing Inductive Proofs. 178-189
  
• Michel Parigot:
  Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. 190-201
  
• Thierry Boy de la Tour, Christoph Kreitz:
  Building Proofs by Analogy via the Curry-Horward Isomorphism. 202-213
  
• Siani Baker, Andrew Ireland, Alan Smaill:
  On the Use of the Constructive Omega-Rule within Automated Deduction. 214-225
  

Parallel Theorem Proving and Logic Programming

• Wolfgang Ertel:
  OR-Parallel Theorem Proving with Random Competition. 226-237
  
• Christian B. Suttner:
  Parallel Computation of Multiple Sets-of_Support. 238-249
  
• Bogumil Hausman:
  Towards Using the Andorra Kernel Language for Industrial Real-Time Applications. 250-260
  

Unification and Equality I

• Christophe Ringeissen:
  Unification in a Combination of Equational Theories with Shared Constants and its Application to Primal Algebras. 261-272
  
• Leo Bachmair, Harald Ganzinger:
  Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. 273-284
  
• Bernhard Gramlich:
  Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems. 285-296
  

Semantics II

• Maurizio Gabbrielli, Giorgio Levi, Daniele Turi:
  A Two Steps Semantics for Logic Programs with Negation. 297-308
  
• Chitta Baral:
  Generalized Negation As Failure and Semantics of Normal Disjunctive Logic Programs. 309-319
  
• Mino Bai, Howard A. Blair:
  General Model Theoretic Semantics for Higher-Order Horn Logic Programming. 320-331
  

Extensions of Logic Programming

• José Alberto Fernández, Jack Minker:
  Disjunctive Deductive Databases. 332-356
  
• Alexander V. Voinov:
  Netlog - A Concept Oriented Logic Programming Language. 357-368
  
• Michael Fisher, Richard Owens:
  From the Past to the Future: Executing Temporal Logic Programs. 369-380
  

Non-Resolution Theorem Proving II

• Christoph Walther:
  Computing Induction Axioms. 381-392
  

Specification and Verification

• Valentin M. Antimirov, Anatoli Degtyarev:
  Consistency of Equational Enrichments. 293-402
  
• Paul Curzon:
  A Programming Logic for a Verified Structured Assembly Language. 403-408
  

Unification and Equality II

• Gernot Salzer:
  The Unification of Infinite Sets of Terms and Its Applications. 409-420
  
• Michael Kohlhase:
  Unification in Order-Sorted Type Theory. 421-432
  
• Andrea Sattler-Klein:
  Infinite, Canonical String Rewriting Systems Generated by Completion. 433-444
  

System Descriptions

• Francis Alexandre, Khaled Bsaïes, Jean-Pierre Finance, Alain Quéré:
  Spes: A System for Logic Program Transformation. 445-447
  
• Jean-Marc Andreoli, Remo Pareschi:
  Linear Objects: a Logic Framework for Open System Programming. 448-450
  
• Bernhard Bauer, Rolf Hennicker:
  ISAR: An Interactive System for Algebraic Implementation Proofs. 451-453
  
• Michael Beeson:
  Mathpert: Computer Support for Learning Algebra, Trig, and Calculus. 454-456
  
• Jorge B. Bocca, Michael Dahmen, Michael Freeston:
  MegaLog - A Platform for Developing Knowledge Base Management Systems. 457-459
  
• Adel Bouhoula, Emmanuel Kounalis, Michaël Rusinowitch:
  SPIKE, an Automatic Theorem Prover. 460-462
  
• Li Dafa:
  An Application to Teaching in Logic Course of ATP Based Natural Deduction. 463-465
  
• Mark Dawson:
  A Generic Logic Environment. 466-468
  
• Michel Dorochevsky, Liang-Liang Li, Mike Reeve, Kees Schuerman, André Véron:
  ElipSys - A Parallel Programming System based on Logic. 469-471
  
• Mireille Ducassé:
  Opium - A High-level Debugging Environment. 472-474
  
• Ulrich Fraus, Heinrich Hußmann:
  An Inductive Theorem Prover Based on Narrowing. 475-477
  
• Terry Gaasterland, Parke Godfrey, Jack Minker, Lev Novik:
  A Cooperative Answering System. 478-480
  
• Javier Leach, Susana Nieva:
  MIZ-PR: A Theorem Prover for Polymorphic and Recursive Functions. 481-483
  
• Pascal Manoury, Michel Parigot, Marianna Simonot:
  ProPre A Programming Language with Proofs. 484-486
  
• Julio García Marrtín, Juan José Moreno-Navarro:
  FRIENDLY-WAM: An Interactive Tool to Understand the Compilation of PROLOG. 487-489
  
• Micha Meier:
  SEPIA - a Bases for Prolog Extensions. 490-492
  
• Hans Nilsson:
  The External Database in SICStus Prolog. 493-495
  
• Jacques Noyé:
  The KCM System: Speeding-up Logic Programming through Hardware Support. 496-498
  
• Igor Romanenko:
  Logican's Workbench. 499-500
  
• Hajime Sawamura, Toshiro Minami, Kyoko Ohashi:
  EUODHILOS: A General Reasoning System for a Variety of Logics. 501-503
  
• Laurent Vieille, Petra Bayer, Volker Küchenhoff, Alexandre Lefebvre, Rainer Manthey:
  The EKS-V1 System. 504-506
  
• Mark Wallace, Thierry Le Provost:
  CHIP and Propia. 507-509