12. CADE 1994: Nancy, France

Alan Bundy (Ed.): Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings. Lecture Notes in Computer Science 814 Springer 1994, ISBN 3-540-58156-1

Invited Talk

John K. Slaney:
The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure. 1-13

Heuristics for Induction

Toby Walsh:
A Divergence Critic. 14-28
Dieter Hutter:
Synthesis of Induction Orderings for Existence Proofs. 29-41
Martin Protzen:
Lazy Generation of Induction Hypotheses. 42-56

Experiments with Resolution Systems

David A. Plaisted:
The Search Efficiency of Theorem Proving Strategies. 57-71
Christophe Bourely, Ricardo Caferra, Nicolas Peltier:
A Method for Building Models Automatically. Experiments with an Extension of OTTER. 72-86
Peter Baumgartner, Ulrich Furbach:
Model Elimination Without Contrapositives. 87-101

Implicit vs. Explicit Induction

François Bronsard, Uday S. Reddy, Robert W. Hasker:
Induction using Term Orderings. 102-117
Jacques Chazarain, Emmanuel Kounalis:
Mechanizable Inductive Proofs for a Class of Forall Exists Formulas. 118-132
Olav Lysne:
On the Connection between Narrowing and Proof by Consistency. 133-147

Induction

Lawrence C. Paulson:
A Fixedpoint Approach to Implementing (Co)Inductive Definitions. 148-161
Claus-Peter Wirth, Bernhard Gramlich:
On Notions of Inductive Validity for First-Oder Equational Clauses. 162-176
Siani Baker:
A New Application for Explanation-Based Generalisation within Automated Deduction. 177-191

Heuristics for Controlling Resolution

Heng Chu, David A. Plaisted:
Semantically Guided First-Order Theorem Proving using Hyper-Linking. 192-206
D. Andre de Waal, John P. Gallagher:
The Applicability of Logic Program Analysis and Transformation to Theorem Proving. 207-221
Stefan Brüning:
Detecting Non-Provable Goals. 222-236

Panel Discussion

Robert S. Boyer:
Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We? 237
The QED Manifesto. 238-251

ATP Problems

Geoff Sutcliffe, Christian B. Suttner, Theodor Yemenis:
The TPTP Problem Library. 252-266

Unification

Eric Domenjoud, Francis Klay, Christophe Ringeissen:
Combination Techniques for Non-Disjoint Equational Theories. 267-281
Gernot Salzer:
Primal Grammars and Unification Modulo a Binary Clause. 282-295

Logic Programming Applications

Koji Iwanuma:
Conservative Query Normalization on Parallel Circumscription. 296-310
Laurent Fribourg, Marcos Veloso Peixoto:
Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints. 311-325
Véronique Royer, Joachim Quantz:
On Intuitionistic Query Answering in Description Bases. 326-340

Applications

Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood:
Deductive Composition of Astronomical Software from Subroutine Libraries. 341-355
William M. Farmer, Joshua D. Guttman, Mark E. Nadel, F. Javier Thayer:
Proof Script Pragmatics in IMPS. 356-370
Manfred Kerber, Michael Kohlhase:
A Mechanization of Strong Kleene Logic for Partial Functions. 371-385

Special-Purpose Provers

Dongming Wang:
Algebraic Factoring and Geometry Proving. 386-400
Nicholas Freitag McPhee, Shang-Ching Chou, Xiao-Shan Gao:
Mechanically Proving Geometry Theorems Using a Combination of Wu's Method and Collins' Method. 401-415
Larry M. Hines:
Str+ve and Integers. 416-430

Banquet Speech

Richard Platek:
What is a Proof? (Abstract). 431

Invited Talk

Ursula Martin:
Termination, Geometry and Invariants. 432-434

Rewrite Rule Termination

Leo Bachmair, Harald Ganzinger:
Ordered Chaining for Total Orderings. 435-450
Aart Middeldorp, Hans Zantema:
Simple Termination Revisited. 451-465
David A. Basin, Toby Walsh:
Termination Orderings for Rippling. 466-483

ATP Efficiency

David B. Sturgill, Alberto Maria Segre:
A Novel Asynchronous Parallelism Scheme for First-Order Logic. 484-498
Jean Goubault:
Proving with BDDs and Control of Information. 499-513
Peter Graf:
Extended Path-Indexing. 514-528

Invited Talk

Robert L. Constable:
Exporting and Refecting Abstract Metamathematics. 529

AC Unification

Laurent Vigneron:
Associative-Commutative Deduction with Constraints. 530-544
Robert Nieuwenhuis, Albert Rubio:
AC-Superposition with Constraints: No AC-Unifiers Needed. 545-559
Miki Hermann, Phokion G. Kolaitis:
The Complexity of Counting Problems in Equational Matching. 560-574

Higher-Order Theorem Proving

Penny Anderson:
Representing Proof Transformations for Program Optimizations. 575-589
Paul Jackson:
Exploring Abstract Algebra in Constructive Type Theory. 590-604
Amy P. Felty, Douglas J. Howe:
Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables. 605-619

Higher-Order Unification

Patricia Johann, Michael Kohlhase:
Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading. 620-634
Christian Prehofer:
Decidable Higher-Order Unification Problems. 635-649
Olaf Müller, Franz Weber:
Theory and Practice of Minimal Modular Higher-Order E-Unification. 650-664

General Unification

Rolf Socher-Ambrosius:
A Refined Version of General E-Unification. 665-677
Bernhard Beckert:
A Completion-Based Method for Mixed Universal and Rigid E-Unification. 678-692
Reinhard Bündgen:
On Pot, Pans and Pudding or How to Discover Generalised Critical Pairs. 693-707

Natural Systems

Stefan Klingenbeck, Reiner Hähnle:
Semantic Tableaux with Ordering Restrictions. 708-722
Fabio Massacci:
Strongly Analytic Tableaux for Normal Modal Logics. 723-737
Xiaorong Huang:
Reconstruction Proofs at the Assertion Level. 738-752

Problem Sets

Jian Zhang:
Problems on the Generation of Finite Models. 753-757
Edmund M. Clarke, Xudong Zhao:
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. 758-763

System Descriptions

John K. Slaney, Ewing L. Lusk, William McCune:
SCOTT: Semantically Constrained Otter System Description. 764-768
Peter Baumgartner, Ulrich Furbach:
PROTEIN: A PROver with a Theory Extension INterface. 769-773
Johann Schumann:
DELTA - A Bottom-up Preprocessor for Top-Down Theorem Provers - System Abstract. 774-777
Christoph Goller, Reinhold Letz, Klaus Mayr, Johann Schumann:
SETHEO V3.2: Recent Developments - System Abstract. 778-782
Wolfgang Bibel, Stefan Brüning, Uwe Egly, Thomas Rath:
KoMeT. 783-787
Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann:
Omega-MKRP: A Proof Development Environment. 788-792
Bernhard Beckert, Joachim Posegga:
leanT^AP: Lean Tableau-Based Theorem Proving (Extended Abstract). 793-797
John K. Slaney:
FINDER: Finite Domain Enumerator - System Description. 798-801
Frederic D. Portoraro:
Symlog: Automated Advice in Fitch-style Proof Construction. 802-806
Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg H. Siekmann:
KEIM: A Toolkit for Automated Deduction. 807-810
Frank Pfenning:
Elf: A Meta-Language for Deductive Systems (System Descrition). 811-815
Takeshi Ohtani, Hajime Sawamura, Toshiro Minami:
EUODHILOS-II on Top of GNU Epoch. 816-820
Lars-Henrik Eriksson:
Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions. 821-825
Bradley L. Richards, Ina Kraan, Alan Smaill, Geraint A. Wiggins:
Mollusc: A General Proof-Development Shell for Sequent-Based Logics. 826-830
Tie-Cheng Wang, Allen Goldberg:
KITP-93: An Automated Inference System for Program Analysis. 831-835
Adel Bouhoula:
SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs. 836-840
Maria Paola Bonacina, William McCune:
Distributed Theorem Proving by Peers. 841-845

Last update Mon May 20 08:57:41 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page