| 1997 | Automated Natural Deduction Prover and Experiments. | Li Dafa |
| 1997 | Hintikka Multiplicities in Matrix Decision Methods for Some Propositional Modal Logics. | Serenella Cerrito, Marta Cialdea Mayer |
| 1997 | A Fast Saturation Strategy for Set-Theoretic Tableaux. | Domenico Cantone |
| 1997 | A Sequent Calculus for Skeptical Default Logic. | Piero A. Bonatti, Nicola Olivetti |
| 1997 | Free Variable Tableaux for Propositional Modal Logics. | Bernhard Beckert, Rajeev Gor |
| 1997 | Tableaux for Diagnosis Applications. | Peter Baumgartner, Peter Frhlich, Ulrich Furbach, Wolfgang Nejdl |
| 1997 | Lean Induction Principles for Tableaux. | Matthias Baaz, Uwe Egly, Christian G. Fermller |
| 1997 | Generalized Tableau Systems for Intemediate Propositional Logics. | Alessandro Avellone, Pierangelo Miglioli, Ugo Moscato, Mario Ornaghi |
| 1997 | Tableaux for Logic Programming with Strong Negation. | Seiki Akama |
| 1996 | Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction. | Andrei Voronkov |
| 1996 | On the Intuitionistic Force of Classical Search (Extended Abstract). | Eike Ritter, David J. Pym, Lincoln A. Wallen |
| 1996 | Distributed Modal Theorem Proving with KE. | Jeremy V. Pitt, Jim Cunningham |
| 1996 | T-String Unification: Unifying Prefixes in Non-classical Proof Methods. | Jens Otten, Christoph Kreitz |
| 1996 | A Tableau Calculus for Minimal Model Reasoning. | Ilkka Niemel |
| 1996 | A Timing Refinement of Intuitionistic Proofs and its Application to the Timing Analysis of Combinational Circuits. | Michael Mendler |
| 1996 | Strong Normalization for All-Style LK. | Jean-Baptiste Joinet, Harold Schellinx, Lorenzo Tortora de Falco |
| 1996 | Efficient Loop-Check for Backward Proof Search in Some Non-classical Propositional Logics. | Alain Heuerding, Michael Seyfried, Heinrich Zimmermann |
| 1996 | Situational Calculus, Linear Connection Proofs and STRIPS-like Planning: An Experimental Comparison. | Bertram Fronhfer |
| 1996 | A Simple Tableau System for the Logic of Elsewhere. | Stphane Demri |
| 1996 | Fibred Tableaux for Multi-Implication Logic. | Marcello D'Agostino, Dov M. Gabbay |
| 1996 | Minimal Model Generation with Positive Unit Hyper-Resolution Tableaux. | Franois Bry, Adnan H. Yahya |
| 1996 | Sequent Calculi for Default and Autoepistemic Logics. | Piero A. Bonatti |
| 1996 | The Disconnection Method - A Confluent Integration of Unification in the Analytic Framework. | Jean-Paul Billon |
| 1996 | Incremental Theory Reasoning Methods for Semantic Tableaux. | Bernhard Beckert, Christian Pape |
| 1996 | Cyclic Connections. | Grard Becher |