11. CADE 1992: Saratoga Springs, NY, USA

Session I: Keynote Address

• Larry Wos:
  The Impossibility of the Automation of Logical Reasoning. 1-3
  

Session II

• Kurt Ammon:
  Automatic Proofs in Mathematical Logic and Analysis. 4-19
  
• Shang-Ching Chou, Xiao-Shan Gao:
  Proving Geometry Statements of Constructive Type. 20-34
  
• Larry M. Hines:
  The Central Variable Strategy of Str+ve. 35-49
  

Session III A

• Franz Baader, Klaus U. Schulz:
  Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. 50-65
  
• Tobias Nipkow, Zhenyu Qian:
  Reduction and Unification in Lambda Calculi with Subtypes. 66-78
  
• Daniel J. Dougherty, Patricia Johann:
  A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract). 79-93
  
• Wolfgang Bibel, Steffen Hölldobler, Jörg Würtz:
  Cycle Unification. 94-108
  

Session III B

• Katherine A. Yelick, Stephen J. Garland:
  A Parallel Completion Procedure for Term Rewriting Systems. 109-123
  
• David A. McAllester:
  Grammar Rewriting. 124-138
  
• Adam Cichon, Pierre Lescanne:
  Polynomial Interpretations and the Complexity of Algorithms. 139-147
  
• Leonidas Fegaras, Tim Sheard, David W. Stemple:
  Uniform Traversal Combinators: Definition, Use and Properties. 148-162
  

Session IV

• Tomás E. Uribe:
  Sorted Unification Using Set Constraints. 163-177
  
• Alan M. Frisch, Anthony G. Cohn:
  An Abstract View of Sorted Unification. 178-192
  
• Alexandre Boudet:
  Unification in Order-Sorted Algebras with Overloading. 193-207
  

Session V: Banquet Address

• Raymond M. Smullyan:
  Puzzles and Paradoxes (Abstract). 208
  

Session VI

• William McCune, Larry Wos:
  Experiments in Automated Deduction with Condensed Detachment. 209-223
  
• Owen L. Astrachan, Mark E. Stickel:
  Caching and Lemmaizing in Model Elimination Theorem Provers. 224-238
  
• Vincent J. Digricoli, Eugene Kochendorfer:
  LIM+ Challenge Problems by RUE Hyper-Resolution. 239-252
  

Session VII

• Peter Jackson:
  Computing Prime Implicates Incrementally. 253-267
  
• Geoff Sutcliffe:
  Linear-Input Subset Analysis. 268-280
  
• Belaid Benhamou, Lakhdar Sais:
  Theoretical Study of Symmetries in Propositional Calculus and Applications. 281-294
  

Session VIII A

• David A. Basin, Toby Walsh:
  Difference Matching. 295-309
  
• Jane Hesketh, Alan Bundy, Alan Smaill:
  Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs. 310-324
  
• Toby Walsh, Alex Nunes, Alan Bundy:
  The Use of Proof Plans to Sum Series. 325-339
  
• Martin Protzen:
  Disproving Conjectures. 340-354
  

Session VIII B

• Mathias Bauer:
  An Interval-based Temporal Logic in a Multivalued Setting. 355-369
  
• Michael Fisher:
  A Normal Form for First-Order Temporal Formulae. 370-384
  
• Ricardo Caferra, Stéphane Demri:
  Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic. 385-399
  
• Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa:
  Embedding Negation as Failure into a Model Generation Theorem Prover. 400-415
  

Session IX

• Robert S. Boyer, Yuan Yu:
  Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. 416-430
  
• Hantao Zhang, Xin Hua:
  Proving the Chinese Remainder Theorem by the Cover Set Induction. 431-445
  
• Peter Madden:
  Automatic Program Optimization Through Proof Transformation. 446-460
  

Session X: Invited Talk

Session XI

• Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder:
  Basic Paramodulation and Superposition. 462-476
  
• Robert Nieuwenhuis, Albert Rubio:
  Theorem Proving with Ordering Constrained Clauses. 477-491
  
• Zohar Manna, Richard J. Waldinger:
  The Special-Relation Rules are Incomplete. 492-506
  
• Bernhard Beckert, Reiner Hähnle:
  An Improved Method for Adding Equality to Free Variable Semantic Tableaux. 507-521
  

Session XII A

• Natarajan Shankar:
  Proof Search in the Intuitionistic Sequent Calculus. 522-536
  
• Frank Pfenning, Ekkehard Rohwedder:
  Implementing the Meta-Theory of Deductive Systems. 537-551
  
• Wilfred Z. Chen:
  Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic. 552-566
  
• William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
  Little Theories. 567-581
  

Session XII B

• Jim Christian:
  Some Termination Criteria for Narrowing and E-Narrowing. 582-588
  
• Nachum Dershowitz, Subrata Mitra, G. Sivakumar:
  Decidable Matching for Convergent Systems (Preliminary Version). 589-602
  
• Delia Kesner:
  Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors. 603-617
  
• R. C. Sekar, I. V. Ramakrishnan:
  Programming with Equations: A Framework for Lazy Parallel Evaluation. 618-632
  

Session XIII

• Anthony G. Cohn:
  A Many Sorted Logic with Possibly Empty Sorts. 633-647
  
• Andrei Voronkov:
  Theorem Proving in Non-Standard Logics Based on the Inverse Method. 648-662
  
• Konstantin Vershinin, Igor Romanenko:
  One More Logic with Uncertainty and Resolution Principle for it. 663-667
  

System Abstracts

• Li Dafa:
  A Natural Deduction Automated Theorem Proving System. 668-672
  
• Tobias Nipkow, Lawrence C. Paulson:
  Isabelle-91. 673-676
  
• Geoff Sutcliffe:
  The Semantically Guided Linear Deduction System. 677-680
  
• Kurt Ammon:
  The SHUNYATA System. 681-685
  
• Shang-Ching Chou:
  A Geometry Theorem Prover for Macintoshes. 686-690
  
• Xin Hua, Hantao Zhang:
  FRI: Failure-Resistant Induction in RRL. 691-695
  
• Hantao Zhang:
  Herky: High Performance Rewriting in RRL. 696-700
  
• William M. Farmer, Joshua D. Guttman, F. Javier Thayer:
  IMPS: System Description. 701-705
  
• Geoffrey D. Alexander, David A. Plaisted:
  Proving Equality Theorems with Hyper-Linking. 706-710
  
• Jawahar Chirimar, Carl A. Gunter, Myra Van Inwegen:
  Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker. 711-715
  
• Dave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill:
  &: Automated Natural Deduction. 716-720
  
• Tomás E. Uribe, Alan M. Frisch, Michael K. Mitchell:
  An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems. 721-725
  
• Dave Barker-Plummer, Alex Rothenberg:
  The GAZER Theorem Prover. 726-730
  
• Ewing L. Lusk, William McCune, John K. Slaney:
  ROO: A Parallel Theorem Prover. 731-734
  
• Tie-Cheng Wang, Allen Goldberg:
  RVF: An Automated Formal Verification System. 735-739
  
• Johann Schumann:
  KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract). 740-742
  
• K. Blackburn:
  A Report in ICL HOL. 743-747
  
• Sam Owre, John M. Rushby, Natarajan Shankar:
  PVS: A Prototype Verification System. 748-752
  
• Wolfgang Reif:
  The KIV System: Systematic Construction of Verified Software. 753-757
  
• Bernhard Beckert, Stefan Gerberding, Reiner Hähnle, Werner Kernig:
  The Tableau-Based Theorem Prover ₃T^AP for Multi-Valued Logics. 758-760
  
• Edmund M. Clarke, Xudong Zhao:
  Analytica - A Theorem Prover in Mathematica. 761-765
  
• Klaus Schneider, Ramayya Kumar, Thomas Kropf:
  The FAUST - Prover. 766-770
  
• Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, Mark Saaltink:
  Eves System Description. 771-775
  
• Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita:
  MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. 776-780
  

Problem Sets

• Ewing L. Lusk, Larry Wos:
  Benchmark Problems in Which Equality Plays the Major Role. 781-785
  
• David A. Randell, Anthony G. Cohn, Zhan Cui:
  Computing Transivity Tables: A Challenge For Automated Theorem Provers. 786-790