13. CADE 1996: New Brunswick, NJ, USA

@proceedings{DBLP:conf/cade/1996,
  editor    = {Michael A. McRobbie and
               John K. Slaney},
  title     = {Automated Deduction - CADE-13, 13th International Conference
               on Automated Deduction, New Brunswick, NJ, USA, July 30 - August
               3, 1996, Proceedings},
  booktitle = {CADE},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1104},
  year      = {1996},
  isbn      = {3-540-61511-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Lecture

• Harald Ganzinger: Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). 1 BibTeX

Session 1A

• Tanel Tammet: A Resolution Theorem Prover for Intuitonistic Logic. 2-16 BibTeX
• Eike Ritter, David J. Pym, Lincoln A. Wallen: Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract). 17-31 BibTeX
• Andrei Voronkov: Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. 32-46 BibTeX

Session 1B

• Andrew Ireland, Alan Bundy: Extensions to a Generalization Critic for Inductive Proof. 47-61 BibTeX
• Jörg Denzinger, Stephan Schulz: Learning Domain Knowledge to Improve Theorem Proving. 62-76 BibTeX
• Martin Protzen: Patching Faulty Conjectures. 77-91 BibTeX

Session 2A

• Erica Melis, Jon Whittle: Internal Analogy in Theorem Proving. 92-105 BibTeX
• Thomas Kolbe, Christoph Walther: Termination of Theorem Proving by Reuse. 106-120 BibTeX
• Claus Sengler: Termination of Algorithms over Non-freely Generated Data Types. 121-135 BibTeX

Session 2B

• Fausto Giunchiglia, Adolfo Villafiorita: ABSFOL: A Proof Checker with Abstraction. 136-140 BibTeX
• Christoph Weidenbach, Bernd Gaede, Georg Rock: SPASS & FLOTTER Version 0.42. 141-145 BibTeX
• Christian B. Suttner, Geoff Sutcliffe: The Design of the CADE-13 ATP System Competition. 146-160 BibTeX
• Hans Jürgen Ohlbach: SCAN - Elimination of Predicate Quantifiers. 161-165 BibTeX
• Dongming Wang: GEOTHER: A Geometry Theorem Prover. 166-170 BibTeX

Session 3A

• David A. Basin, Seán Matthews: Structuring Metatheory on Inductive Definitions. 171-185 BibTeX
• Ole Rasmussen: An Embedding of Ruby in Isabelle. 186-200 BibTeX
• Peter V. Homeier, David F. Martin: Mechanical Verification of Mutually Recursive Procedures. 201-215 BibTeX

Session 3B

• Giovanni Felici, Giovanni Rinaldi, Klaus Truemper: FasTraC: A Decentralized Traffic Control System Based on Logic Programming. 216-220 BibTeX
• Xiaorong Huang, Armin Fiedler: Presenting Machine-Found Proofs. 221-225 BibTeX
• Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach: MUltlog 1.0: Towards an Expert System for Many-Valued Logics. 226-230 BibTeX
• Janet Bertot, Yves Bertot: CtCoq: A System Presentation. 231-234 BibTeX
• Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang: An Introduction to Geometry Expert. 235-239 BibTeX
• Johann Schumann: SiCoTHEO: Simple Competitive Parallel Theorem Provers. 240-244 BibTeX

Invited Lecture

• Dana S. Scott: What Can We Hope to Achieve From Automated Deduction? (Abstract). 245 BibTeX

Session 4A

• Miki Hermann, Phokion G. Kolaitis: Unification Algorithms Cannot be Combined in Polynomial Time. 246-260 BibTeX
• Qing Guo, Paliath Narendran, David A. Wolfram: Unification and Matching Modulo Nilpotence. 261-274 BibTeX
• Sergei G. Vorobyov: An Improved Lower Bound for the Elementary Theories of Trees. 275-287 BibTeX

Session 4B

• Dieter Hutter, Claus Sengler: INKA: The Next Generation. 288-292 BibTeX
• Torsten Schaub, Stefan Brüning, Pascal Nicolas: XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description. 293-297 BibTeX
• William M. Farmer, Joshua D. Guttman, F. Javier Thayer: IMPS: An Updated System Description. 298-302 BibTeX
• Bernhard Beckert, Reiner Hähnle, Peter Oel, Martin Sulzmann: The Tableau-based Theorem Prover ₃T^AP Version 4.0. 303-307 BibTeX
• Jian Zhang, Hantao Zhang: System Description: Generating Models by SEM. 308-312 BibTeX

Session 5A

• John Harrison: Optimizing Proof Search in Model Elimination. 313-327 BibTeX
• Konstantinos F. Sagonas, Terrance Swift, David Scott Warren: An Abstract Machine for Fixed-Order Dynamically Stratified Programs. 328-342 BibTeX
• Christoph Weidenbach: Unification in Pseudo-Linear Sort Theories is Decidable. 343-357 BibTeX

Session 5B

• Ursula Martin: Theorem Proving with Group Presentations: Examples and Questions. 358-372 BibTeX
• Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema: Transforming Termination by Self-Labelling. 373-387 BibTeX
• Harald Ganzinger, Uwe Waldmann: Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). 388-402 BibTeX

Session 6A

• Uwe Egly, Thomas Rath: On the Practical Value of Different Definitional Translations to Normal Form. 403-417 BibTeX
• Stephan Schmitt, Christoph Kreitz: Converting Non-Classical Matrix Proofs into Sequent-Style Systems. 418-432 BibTeX
• Heribert Schütz, Tim Geisler: Efficient Model Generation through Compilation. 433-447 BibTeX

Session 6B

• Steve Linton, Ursula Martin, Péter Pröhle, Duncan Shand: Algebra and Automated Deduction. 448-462 BibTeX
• David Cyrluk, Patrick Lincoln, Natarajan Shankar: On Shostak's Decision Procedure for Combinations of Theories. 463-477 BibTeX
• Thierry Boy de la Tour: Ground Resolution with Group Computations on Semantic Symmetries. 478-492 BibTeX

Session 7A

• Olivier Roussel, Philippe Mathieu: A New Method for Knowledge Compilation: The Achievement by Cycle Search. 493-507 BibTeX
• Wayne Snyder, James G. Schmolze: Rewrite Semantics for Production Rule Systems: Theory and Applications. 508-522 BibTeX
• Matthias Fuchs: Experiments in the Heuristic Use of Past Proof Experience. 523-537 BibTeX

Session 7B

• Deepak Kapur, Mahadevan Subramaniam: Lemma Discovery in Automated Induction. 538-552 BibTeX
• Peter Graf, Christoph Meyer: Advanced Indexing Operations on Substitution Trees. 553-567 BibTeX
• Christian G. Fermüller: Semantic Trees Revisited: Some New Completeness Results. 568-582 BibTeX

Session 8A

• Fausto Giunchiglia, Roberto Sebastiani: Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. 583-597 BibTeX
• Andreas Nonnengart: Resolution-Based Calculi for Modal and Temporal Logics. 598-612 BibTeX
• Giuseppe De Giacomo, Fabio Massacci: Tableaux and Algorithms for Propositional Dynamic Logic with Converse. 613-627 BibTeX

Session 8B

• Harald Rueß: Reflection of Formal Tactics in a Deductive Reflection Framework. 628-642 BibTeX
• David A. McAllester, Kostas Arkoudas: Walther Recursion. 643-657 BibTeX
• Amy P. Felty: Proof Search with Set Variable Instantiation in the Calculus of Constructions. 658-672 BibTeX

Session 9A

• Clare Dixon: Search Strategies for Resolution in Temporal Logics. 673-687 BibTeX
• Gernot Salzer: Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices. 688-702 BibTeX
• Saturnino F. Luz-Filho: Grammar Specification in Categorial Logics and Theorem Proving. 703-717 BibTeX

Session 9B

• Peter Graf: Path Indexing for AC-Theories. 718-732 BibTeX
• Tobias Nipkow: More Church-Rosser Proofs (in Isabelle/HOL). 733-747 BibTeX
• Tai Joon Park, Allen Van Gelder: Partitioning Methods for Satisfiability Testing on Large Formulas. 748-762 BibTeX