default search action
12th CADE 1994: Nancy, France
- Alan Bundy:
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 - anonymous:
The QED Manifesto. 238-251
ATP Problems
- Geoff Sutcliffe
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
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 B. 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:
leanTAP: 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-22 18:47 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: