Research Catalog

Title

Automated deduction, CADE-12 : 12th International Conference on Automated Deduction, Nancy, France, June 26-July 1, 1994 : proceedings / Alan Bundy, ed.

Author

International Conference on Automated Deduction (12th : 1994 : Nancy, France)

Publication

Berlin ; New York : Springer-Verlag, ©1994.

Items in the Library & Off-site

Details

Additional Authors

Bundy, Alan.

Description

xvi, 848 pages : illustrations; 24 cm

Summary

"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.

Series Statement

Lecture notes in computer science ; 814. Lecture notes in artificial intelligence

Uniform Title

• Lecture notes in computer science ; 814.
• Lecture notes in computer science. Lecture notes in artificial intelligence.

Alternative Title

CADE-12

Subject

• Automatic theorem proving > Congresses
• Logic, Symbolic and mathematical > Congresses
• Automatic theorem proving
• Logic, Symbolic and mathematical
• Automatisches Beweisverfahren
• Kongress
• Automatische bewijsvoering

Genre/Form

• Conference papers and proceedings.
• Nancy (1994)

Bibliography (note)

• Includes bibliographical references and index.

Contents

• 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.

ISBN

• 3540581561
• 9783540581567
• 0387581561
• 9780387581569

LCCN

94017912

OCLC

• ocm30544565
• 30544565
• SCSB-2024245

Owning Institutions

Princeton University Library