13. CADE 1996: New Brunswick, NJ, USA

Invited Lecture

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

Session 1A

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

Session 1B

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

Session 2A

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

Session 2B

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

Session 3A

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

Session 3B

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

Invited Lecture

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

Session 4A

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

Session 4B

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

Session 5A

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

Session 5B

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

Session 6A

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

Session 6B

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

Session 7A

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

Session 7B

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

Session 8A

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

Session 8B

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

Session 9A

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

Session 9B

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

Last update Mon May 20 08:57:43 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page