Michael A. McRobbie, John K. Slaney
Proceedings of the 13th International Conference on Automated Deduction
CADE, 1996.

@proceedings{CADE-1996,
	address       = "New Brunswick, New Jersey, USA",
	editor        = "Michael A. McRobbie and John K. Slaney",
	isbn          = "3-540-61511-3",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 13th International Conference on Automated Deduction}",
	volume        = 1104,
	year          = 1996,
}

Contents (63 items)

20 ×#proving
12 ×#theorem proving
9 ×#named
8 ×#logic
3 ×#algorithm
3 ×#automation
3 ×#deduction
3 ×#generative
3 ×#induction
3 ×#semantics

CADE-1996-Ganzinger #proving #theorem proving

Saturation-Based Theorem Proving: Past Successes and Future Potential (HG), p. 1.

CADE-1996-Tammet #logic #proving #theorem proving

A Resolution Theorem Prover for Intuitonistic Logic (TT), pp. 2–16.

CADE-1996-RitterPW

Proof-Terms for Classical and Intuitionistic Resolution (ER, DJP, LAW), pp. 17–31.

CADE-1996-Voronkov #logic #similarity

Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification (AV), pp. 32–46.

CADE-1996-IrelandB #induction #proving

Extensions to a Generalization Critic for Inductive Proof (AI, AB), pp. 47–61.

CADE-1996-DenzingerS #learning #proving #theorem proving

Learning Domain Knowledge to Improve Theorem Proving (JD, SS), pp. 62–76.

CADE-1996-Protzen

Patching Faulty Conjectures (MP), pp. 77–91.

CADE-1996-MelisW #proving #theorem proving

Internal Analogy in Theorem Proving (EM, JW), pp. 92–105.

CADE-1996-KolbeW #proving #reuse #termination #theorem proving

Termination of Theorem Proving by Reuse (TK, CW), pp. 106–120.

CADE-1996-Sengler #algorithm #data type #termination

Termination of Algorithms over Non-freely Generated Data Types (CS), pp. 121–135.

CADE-1996-GiunchigliaV #abstraction #named #proving

ABSFOL: A Proof Checker with Abstraction (FG, AV), pp. 136–140.

CADE-1996-WeidenbachGR

SPASS & FLOTTER Version 0.42 (CW, BG, GR), pp. 141–145.

CADE-1996-SuttnerS #contest #design

The Design of the CADE-13 ATP System Competition (CBS, GS), pp. 146–160.

CADE-1996-Ohlbach #named #quantifier

SCAN — Elimination of Predicate Quantifiers (HJO), pp. 161–165.

CADE-1996-Wang #geometry #named #proving #theorem proving

GEOTHER: A Geometry Theorem Prover (DW), pp. 166–170.

CADE-1996-BasinM #induction

Structuring Metatheory on Inductive Definitions (DAB, SM), pp. 171–185.

CADE-1996-Rasmussen #ruby

An Embedding of Ruby in Isabelle (OR), pp. 186–200.

CADE-1996-HomeierM #recursion #verification

Mechanical Verification of Mutually Recursive Procedures (PVH, DFM), pp. 201–215.

CADE-1996-FeliciRT #distributed #logic programming #named

FasTraC: A Decentralized Traffic Control System Based on Logic Programming (GF, GR, KT), pp. 216–220.

CADE-1996-HuangF #proving

Presenting Machine-Found Proofs (XH, AF), pp. 221–225.

CADE-1996-BaazFSZ #logic #towards

MUltlog 1.0: Towards an Expert System for Many-Valued Logics (MB, CGF, GS, RZ), pp. 226–230.

CADE-1996-BertotB #named

CtCoq: A System Presentation (JB, YB), pp. 231–234.

CADE-1996-ChouGZ #geometry

An Introduction to Geometry Expert (SCC, XSG, JZZ), pp. 235–239.

CADE-1996-Schumann #named #parallel #proving #theorem proving

SiCoTHEO: Simple Competitive Parallel Theorem Provers (JS), pp. 240–244.

CADE-1996-Scott #automation #deduction #question #what

What Can We Hope to Achieve From Automated Deduction? (DSS), p. 245.

CADE-1996-HermannK #algorithm #polynomial #unification

Unification Algorithms Cannot be Combined in Polynomial Time (MH, PGK), pp. 246–260.

CADE-1996-GuoNW #unification

Unification and Matching Modulo Nilpotence (QG, PN, DAW), pp. 261–274.

CADE-1996-Vorobyov #bound

An Improved Lower Bound for the Elementary Theories of Trees (SGV), pp. 275–287.

CADE-1996-HutterS #generative #named

INKA: The Next Generation (DH, CS), pp. 288–292.

CADE-1996-SchaubBN #named #prolog #proving #reasoning #theorem proving

XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description (TS, SB, PN), pp. 293–297.

CADE-1996-FarmerGF #named

IMPS: An Updated System Description (WMF, JDG, FJT), pp. 298–302.

CADE-1996-BeckertHOS #proving #theorem proving

The Tableau-based Theorem Prover 3TAP Version 4.0 (BB, RH, PO, MS), pp. 303–307.

CADE-1996-ZhangZ #generative #modelling

System Description: Generating Models by SEM (JZ, HZ), pp. 308–312.

CADE-1996-Harrison #optimisation #proving

Optimizing Proof Search in Model Elimination (JH), pp. 313–327.

CADE-1996-SagonasSW #automaton #source code

An Abstract Machine for Fixed-Order Dynamically Stratified Programs (KFS, TS, DSW), pp. 328–342.

CADE-1996-Weidenbach #decidability #pseudo #unification

Unification in Pseudo-Linear Sort Theories is Decidable (CW), pp. 343–357.

CADE-1996-Martin #proving #theorem proving

Theorem Proving with Group Presentations: Examples and Questions (UM), pp. 358–372.

CADE-1996-MiddeldorpOZ #self #termination

Transforming Termination by Self-Labelling (AM, HO, HZ), pp. 373–387.

CADE-1996-GanzingerW #monad #proving #theorem proving

Theorem Proving in Cancellative Abelian Monoids (HG, UW), pp. 388–402.

CADE-1996-EglyR #normalisation #on the

On the Practical Value of Different Definitional Translations to Normal Form (UE, TR), pp. 403–417.

CADE-1996-SchmittK #matrix #proving

Converting Non-Classical Matrix Proofs into Sequent-Style Systems (SS, CK), pp. 418–432.

CADE-1996-SchutzG #compilation #generative #performance

Efficient Model Generation through Compilation (HS, TG), pp. 433–447.

CADE-1996-LintonMPS #algebra #automation #deduction

Algebra and Automated Deduction (SL, UM, PP, DS), pp. 448–462.

CADE-1996-CyrlukLS #on the

On Shostak’s Decision Procedure for Combinations of Theories (DC, PL, NS), pp. 463–477.

CADE-1996-Tour #semantics #symmetry

Ground Resolution with Group Computations on Semantic Symmetries (TBdlT), pp. 478–492.

CADE-1996-RousselM #compilation

A New Method for Knowledge Compilation: The Achievement by Cycle Search (OR, PM), pp. 493–507.

CADE-1996-SnyderS #semantics #theory and practice

Rewrite Semantics for Production Rule Systems: Theory and Applications (WS, JGS), pp. 508–522.

CADE-1996-Fuchs #experience #heuristic #proving #using

Experiments in the Heuristic Use of Past Proof Experience (MF), pp. 523–537.

CADE-1996-KapurS #automation #induction

Lemma Discovery in Automated Induction (DK, MS), pp. 538–552.

CADE-1996-GrafM

Advanced Indexing Operations on Substitution Trees (PG, CM), pp. 553–567.

CADE-1996-Fernmuller #semantics

Semantic Trees Revisited: Some New Completeness Results (CGF), pp. 568–582.

CADE-1996-GiunchigliaS #case study #logic

Building Decision Procedures for Modal Logics from Propositional Decision Procedure — The Case Study of Modal K (FG, RS), pp. 583–597.

CADE-1996-Nonnengart #calculus #logic

Resolution-Based Calculi for Modal and Temporal Logics (AN), pp. 598–612.

CADE-1996-GiacomoM #algorithm #logic

Tableaux and Algorithms for Propositional Dynamic Logic with Converse (GDG, FM), pp. 613–627.

CADE-1996-Ruess #deduction #framework

Reflection of Formal Tactics in a Deductive Reflection Framework (HR), pp. 628–642.

CADE-1996-McAllesterA #recursion

Walther Recursion (DAM, KA), pp. 643–657.

CADE-1996-Felty #calculus #proving #set

Proof Search with Set Variable Instantiation in the Calculus of Constructions (APF), pp. 658–672.

CADE-1996-Dixon #logic

Search Strategies for Resolution in Temporal Logics (CD), pp. 673–687.

CADE-1996-Salzer #axiom #multi #quantifier

Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices (GS), pp. 688–702.

CADE-1996-Luz-Filho #logic #proving #specification #theorem proving

Grammar Specification in Categorial Logics and Theorem Proving (SFLF), pp. 703–717.

CADE-1996-Graf

Path Indexing for AC-Theories (PG), pp. 718–732.

CADE-1996-Nipkow #higher-order #proving

More Church-Rosser Proofs (in Isabelle/HOL) (TN), pp. 733–747.

CADE-1996-ParkG #clustering #satisfiability #scalability #testing

Partitioning Methods for Satisfiability Testing on Large Formulas (TJP, AVG), pp. 748–762.