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 updated on Tue May 21 01:52:54 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page