13. CADE 1996:
New Brunswick, NJ, USA
: Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract).
: A Resolution Theorem Prover for Intuitonistic Logic.
: Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification.
: Termination of Algorithms over Non-freely Generated Data Types.
Dana S. Scott
: What Can We Hope to Achieve From Automated Deduction? (Abstract).
: Theorem Proving with Group Presentations: Examples and Questions.
, Thomas Rath
: On the Practical Value of Different Definitional Translations to Normal Form.
: Experiments in the Heuristic Use of Past Proof Experience.
: Reflection of Formal Tactics in a Deductive Reflection Framework.
Amy P. Felty
: Proof Search with Set Variable Instantiation in the Calculus of Constructions.
: Search Strategies for Resolution in Temporal Logics.
: Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices.
: Path Indexing for AC-Theories.
: More Church-Rosser Proofs (in Isabelle/HOL).