Automated Deduction - Cade-12: 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994. Proceedings (Lecture Notes in Computer Science / Lecture Notes in Artific)

This Volume Contains The Reviewed Papers Presented At The 12th International Conference On Automated Deduction (cade-12) Held At Nancy, France In June/july 1994. The 67 Papers Presented Were Selected From 177 Submissions And Document Many Of The Most Important Research Results In Automated Deduction Since Cade-11 Was Held In June 1992. The Volume Is Organized In Chapters On Heuristics, Resolution Systems, Induction, Controlling Resolutions, Atp Problems, Unification, Lp Applications, Special-purpose Provers, Rewrite Rule Termination, Atp Efficiency, Ac Unification, Higher-order Theorem Proving, Natural Systems, Problem Sets, And System Descriptions.--publisher's Website. The Crisis In Finite Mathematics: Automated Reasoning As Cause And Cure / John Slaney -- A Divergence Critic / Toby Walsh -- Synthesis Of Induction Orderings For Existence Proofs / Dieter Hutter -- Lazy Generation Of Induction Hypotheses / Martin Protzen -- The Search Efficiency Of Theorem Proving Strategies / David A. Plaisted -- A Method For Building Models Automatically: Experiments With An Extension Of Otter / Christophe Bourely, Ricardo Caferra And Nicolas Peltier -- Model Elimination Without Contrapositives / Peter Baumgartner And Ulrich Furbach -- Induction Using Term Orderings / Francois Bronsard, Uday S. Reddy And Robert W. Hasker -- Mechanizable Inductive Proofs For A Class Of [actual Symbol Not Reproducible] Formulas / Jacques Chazarain And Emmanuel Kounalis -- On The Connection Between Narrowing And Proof By Consistency / Olav Lysne -- A Fixedpoint Approach To Implementing (co)inductive Definitions / Lawrence C. Paulson. On Notions Of Inductive Validity For First-order Equational Clauses / Claus-peter Wirth And Bernhard Gramlich -- A New Application For Explanation-based Generalisation Within Automated Deduction / Siani Baker -- Semantically Guided First-order Theorem Proving Using Hyper-linking / Heng Chu And David A. Plaisted -- The Applicability Of Logic Program Analysis And Transformation To Theorem Proving / D.a. De Waal And J.p. Gallagher -- Detecting Non-provable Goals / Stefan Bruning -- A Mechanically Proof-checked Encyclopedia Of Mathematics: Should We Build One? Can We? / Robert S. Boyer, N.g. De Bruijn, Gerard Huet And Andrzej Trybulec -- The Tptp Problem Library / Geoff Sutcliffe, Christian Suttner And Theodor Yemenis -- Combination Techniques For Non-disjoint Equational Theories / Eric Domenjoud, Francis Klay And Christophe Ringeissen -- Primal Grammars And Unification Modulo A Binary Clause / Gernot Salzer -- Conservative Query Normalization On Parallel Circumscription / Kouji Iwanuma. Bottom-up Evaluation Of Datalog Programs With Arithmetic Constraints / Laurent Fribourg And Marcos Veloso Peixoto -- On Intuitionistic Query Answering In Description Bases / Veronique Royer And J. Joachim Quantz -- Deductive Composition Of Astronomical Software From Subroutine Libraries / Mark Stickel, Richard Waldinger, Michael Lowry, Thomas Pressburger And Ian Underwood -- Proof Script Pragmatics In Imps / William M. Farmer, Joshua D. Guttman, Mark E. Nadel And F. Javier Thayer -- A Mechanization Of Strong Kleene Logic For Partial Functions / Manfred Kerber And Michael Kohlhase -- Algebraic Factoring And Geometry Theorem Proving / Dongming Wang -- Mechanically Proving Geometry Theorems Using A Combination Of Wu's Method And Collins' Method / Nicholas Freitag Mcphee, Shang-ching Chou And Xiao-shan Gao -- Strive And Integers / Larry M. Hines -- What Is A Proof? / Richard Platek -- Termination, Geometry And Invariants / Ursula Martin. Ordered Chaining For Total Orderings / Leo Bachmair And Harald Ganzinger -- Simple Termination Revisited / Aart Middeldorp And Hans Zantema -- Termination Orderings For Rippling / David A. Basin And Toby Walsh -- A Novel Asynchronous Parallelism Scheme For First-order Logic / David B. Sturgill And Alberto Maria Segre -- Proving With Bdds And Control Of Information / Jean Goubault -- Extended Path-indexing / Peter Graf -- Exporting And Reflecting Abstract Metamathematics / Robert L. Constable -- Associative-commutative Deduction With Constraints / Laurent Vigneron -- Ac-superposition With Constraints: No Ac-unifiers Needed / Robert Nieuwenhuis And Albert Rubio -- The Complexity Of Counting Problems In Equational Matching / Miki Hermann And Phokion G. Kolaitis -- Representing Proof Transformations For Program Optimization / Penny Anderson -- Exploring Abstract Algebra In Constructive Type Theory / Paul Jackson. Tactic Theorem Proving With Refinement-tree Proofs And Metavariables / Amy Felty And Douglas Howe -- Unification In An Extensional Lambda Calculus With Ordered Function Sorts And Constant Overloading / Patricia Johann And Michael Kohlhase -- Decidable Higher-order Unification Problems / Christian Prehofer -- Theory And Practice Of Minimal Modular Higher-order E-unification / Olaf Muller And Franz Weber -- A Refined Version Of General E-unification / Rolf Socher-ambrosius -- A Completion-based Method For Mixed Universal And Rigid E-unification / Bernhard Beckert -- On Pot, Pans And Pudding Or How To Discover Generalised Critical Pairs / Reinhard Bundgen -- Semantic Tableaux With Ordering Restrictions / Stefan Klingenbeck And Reiner Hahnle -- Strongly Analytic Tableaux For Normal Modal Logics / Fabio Massacci -- Reconstructing Proofs At The Assertion Level / Xiaorong Huang -- Problems On The Generation Of Finite Models / Jian Zhang. Combining Symbolic Computation And Theorem Proving: Some Problems Of Ramanujan / Edmund Clarke And Xudong Zhao -- Scott: Semantically Constrained Otter / John Slaney, Ewing Lusk And William W. Mccune -- Protein: A Prover With A Theory Extension Interface / Peter Baumgartner And Ulrich Furbach -- Delta -- A Bottom-up Preprocessor For Top-down Theorem Provers / Johann M. Ph. Schumann -- Setheo V3.2: Recent Developments / Ch. Goller, R. Letz, K. Mayr And Johann M. Ph. Schumann -- Komet / W. Bibel, Stefan Bruning, U. Egly And T. Rath -- [omega]-mkrp: A Proof Development Environment / Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jorn Richts And Jorg Siekmann -- Leantap: Lean Tableau-based Theorem Proving / Bernhard Beckert And Joachim Posegga -- Finder: Finite Domain Enumerator / John Slaney -- Symlog: Automated Advice In Fitch-style Proof Construction / Frederic D. Portoraro. Keim: A Toolkit For Automated Deduction / Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jorn Richts And Jorg Siekmann -- Elf: A Meta-language For Deductive Systems / Frank Pfenning -- Euodhilos-ii On Top Of Gnu Epoch / Takeshi Ohtani, Hajime Sawamura And Toshiro Minami -- Pi: An Interactive Derivation Editor For The Calculus Of Partial Inductive Definitions / Lars-henrik Eriksson -- Mollusc: A General Proof-development Shell For Sequent-based Logics / Bradley L. Richards, Ina Kraan, Alan Smaill And Geraint A. Wiggins -- Kitp-93: An Automated Inference System For Program Analysis / T. C. Wang And Allen Goldberg -- Spike: A System For Sufficient Completeness And Parameterized Inductive Proofs / Adel Bouhoula -- Distributed Theorem Proving By Peers / Maria Paola Bonacina And William W. Mccune. Alan Bundy, Ed. Includes Bibliographical References And Index. The crisis in finite mathematics: Automated reasoning as cause and cure....Pages 1-13 A divergence critic....Pages 14-28 Synthesis of induction orderings for existence proofs....Pages 29-41 Lazy generation of induction hypotheses....Pages 42-56 The search efficiency of theorem proving strategies....Pages 57-71 A method for building models automatically. Experiments with an extension of OTTER....Pages 72-86 Model elimination without contrapositives....Pages 87-101 Induction using term orderings....Pages 102-117 Mechanizable inductive proofs for a class of ∀ ∃ formulas....Pages 118-132 On the connection between narrowing and proof by consistency....Pages 133-147 A fixedpoint approach to implementing (Co)inductive definitions....Pages 148-161 On notions of inductive validity for first-order equational clauses....Pages 162-176 A new application for explanation-based generalisation within automated deduction....Pages 177-191 Semantically guided first-order theorem proving using hyper-linking....Pages 192-206 The applicability of logic program analysis and transformation to theorem proving....Pages 207-221 Detecting non-provable goals....Pages 222-236 A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?....Pages 237-251 The TPTP problem library....Pages 252-266 Combination techniques for non-disjoint equational theories....Pages 267-281 Primal grammars and unification modulo a binary clause....Pages 282-295 Conservative query normalization on parallel circumscription....Pages 296-310 Bottom-up evaluation of Datalog programs with arithmetic constraints....Pages 311-325 On intuitionistic query answering in description bases....Pages 326-340 Deductive composition of astronomical software from subroutine libraries....Pages 341-355 Proof script pragmatics in IMPS....Pages 356-370 A mechanization of strong Kleene logic for partial functions....Pages 371-385 Algebraic factoring and geometry theorem proving....Pages 386-400 Mechanically proving geometry theorems using a combination of Wu's method and Collins' method....Pages 401-415 Str∔ve and integers....Pages 416-430 What is a proof?....Pages 431-431 Termination, geometry and invariants....Pages 432-434 Ordered chaining for total orderings....Pages 435-450 Simple termination revisited....Pages 451-465 Termination orderings for rippling....Pages 466-483 A novel asynchronous parallelism scheme for first-order logic....Pages 484-498 Proving with BDDs and control of information....Pages 499-513 Extended path-indexing....Pages 514-528 Exporting and reflecting abstract metamathematics....Pages 529-529 Associative-commutative deduction with constraints....Pages 530-544 AC-superposition with constraints: No AC-unifiers needed....Pages 545-559 The complexity of counting problems in equational matching....Pages 560-574 Representing proof transformations for program optimization....Pages 575-589 Exploring abstract algebra in constructive type theory....Pages 590-604 Tactic theorem proving with refinement-tree proofs and metavariables....Pages 605-619 Unification in an extensional lambda calculus with ordered function sorts and constant overloading....Pages 620-634 Decidable higher-order unification problems....Pages 635-649 Theory and practice of minimal modular higher-order E -unification....Pages 650-664 A refined version of general E-unification....Pages 665-677 A completion-based method for mixed universal and rigid E -unification....Pages 678-692 On pot, pans and pudding or how to discover generalised critical Pairs....Pages 693-707 Semantic tableaux with ordering restrictions....Pages 708-722 Strongly analytic tableaux for normal modal logics....Pages 723-737 Reconstructing proofs at the assertion level....Pages 738-752 Problems on the generation of finite models....Pages 753-757 Combining symbolic computation and theorem proving: Some problems of Ramanujan....Pages 758-763 SCOTT: Semantically constrained otter system description....Pages 764-768 Protein: A PRO ver with a T heory E xtension IN terface....Pages 769-773 DELTA — A bottom-up preprocessor for top-down theorem provers....Pages 774-777 SETHEO V3.2: Recent developments....Pages 778-782 KoMeT....Pages 783-787 Ω-MKRP: A proof development environment....Pages 788-792 Lean T A P : Lean tableau-based theorem proving....Pages 793-797 FINDER: Finite domain enumerator system description....Pages 798-801 Symlog automated advice in Fitch-style proof construction....Pages 802-806 KEIM: A toolkit for automated deduction....Pages 807-810 Elf: A meta-language for deductive systems....Pages 811-815 EUODHILOS-II on top of GNU epoch....Pages 816-820 Pi: An interactive derivation editor for the calculus of partial inductive definitions....Pages 821-825 Mollusc a general proof-development shell for sequent-based logics....Pages 826-830 KITP-93: An automated inference system for program analysis....Pages 831-835 SPIKE: A system for sufficient completeness and parameterized inductive proofs....Pages 836-840 Distributed theorem proving by Peers ....Pages 841-845