↓ Skip to main content

Automated Deduction, Cade-12.

Overview of attention for book
Cover of 'Automated Deduction, Cade-12.'

Table of Contents

  1. Altmetric Badge
    Book Overview
  2. Altmetric Badge
    Chapter 1 The crisis in finite mathematics: Automated reasoning as cause and cure
  3. Altmetric Badge
    Chapter 2 A divergence critic
  4. Altmetric Badge
    Chapter 3 Synthesis of induction orderings for existence proofs
  5. Altmetric Badge
    Chapter 4 Lazy generation of induction hypotheses
  6. Altmetric Badge
    Chapter 5 The search efficiency of theorem proving strategies
  7. Altmetric Badge
    Chapter 6 A method for building models automatically. Experiments with an extension of OTTER
  8. Altmetric Badge
    Chapter 7 Model elimination without contrapositives
  9. Altmetric Badge
    Chapter 8 Induction using term orderings
  10. Altmetric Badge
    Chapter 9 Mechanizable inductive proofs for a class of ∀ ∃ formulas
  11. Altmetric Badge
    Chapter 10 On the connection between narrowing and proof by consistency
  12. Altmetric Badge
    Chapter 11 Automated Deduction — CADE-12
  13. Altmetric Badge
    Chapter 12 On notions of inductive validity for first-order equational clauses
  14. Altmetric Badge
    Chapter 13 A new application for explanation-based generalisation within automated deduction
  15. Altmetric Badge
    Chapter 14 Semantically guided first-order theorem proving using hyper-linking
  16. Altmetric Badge
    Chapter 15 The applicability of logic program analysis and transformation to theorem proving
  17. Altmetric Badge
    Chapter 16 Detecting non-provable goals
  18. Altmetric Badge
    Chapter 17 A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?
  19. Altmetric Badge
    Chapter 18 The TPTP problem library
  20. Altmetric Badge
    Chapter 19 Combination techniques for non-disjoint equational theories
  21. Altmetric Badge
    Chapter 20 Primal grammars and unification modulo a binary clause
  22. Altmetric Badge
    Chapter 21 Conservative query normalization on parallel circumscription
  23. Altmetric Badge
    Chapter 22 Bottom-up evaluation of Datalog programs with arithmetic constraints
  24. Altmetric Badge
    Chapter 23 On intuitionistic query answering in description bases
  25. Altmetric Badge
    Chapter 24 Deductive composition of astronomical software from subroutine libraries
  26. Altmetric Badge
    Chapter 25 Proof script pragmatics in IMPS
  27. Altmetric Badge
    Chapter 26 A mechanization of strong Kleene logic for partial functions
  28. Altmetric Badge
    Chapter 27 Algebraic factoring and geometry theorem proving
  29. Altmetric Badge
    Chapter 28 Mechanically proving geometry theorems using a combination of Wu's method and Collins' method
  30. Altmetric Badge
    Chapter 29 Str∔ve and integers
  31. Altmetric Badge
    Chapter 30 What is a proof?
  32. Altmetric Badge
    Chapter 31 Termination, geometry and invariants
  33. Altmetric Badge
    Chapter 32 Ordered chaining for total orderings
  34. Altmetric Badge
    Chapter 33 Simple termination revisited
  35. Altmetric Badge
    Chapter 34 Termination orderings for rippling
  36. Altmetric Badge
    Chapter 35 A novel asynchronous parallelism scheme for first-order logic
  37. Altmetric Badge
    Chapter 36 Proving with BDDs and control of information
  38. Altmetric Badge
    Chapter 37 Extended path-indexing
  39. Altmetric Badge
    Chapter 38 Exporting and reflecting abstract metamathematics
  40. Altmetric Badge
    Chapter 39 Associative-commutative deduction with constraints
  41. Altmetric Badge
    Chapter 40 AC-superposition with constraints: No AC-unifiers needed
  42. Altmetric Badge
    Chapter 41 The complexity of counting problems in equational matching
  43. Altmetric Badge
    Chapter 42 Representing proof transformations for program optimization
  44. Altmetric Badge
    Chapter 43 Exploring abstract algebra in constructive type theory
  45. Altmetric Badge
    Chapter 44 Tactic theorem proving with refinement-tree proofs and metavariables
  46. Altmetric Badge
    Chapter 45 Unification in an extensional lambda calculus with ordered function sorts and constant overloading
  47. Altmetric Badge
    Chapter 46 Decidable higher-order unification problems
  48. Altmetric Badge
    Chapter 47 Theory and practice of minimal modular higher-order E -unification
  49. Altmetric Badge
    Chapter 48 A refined version of general E-unification
  50. Altmetric Badge
    Chapter 49 A completion-based method for mixed universal and rigid E -unification
  51. Altmetric Badge
    Chapter 50 On pot, pans and pudding or how to discover generalised critical Pairs
  52. Altmetric Badge
    Chapter 51 Semantic tableaux with ordering restrictions
  53. Altmetric Badge
    Chapter 52 Strongly analytic tableaux for normal modal logics
  54. Altmetric Badge
    Chapter 53 Reconstructing proofs at the assertion level
  55. Altmetric Badge
    Chapter 54 Problems on the generation of finite models
  56. Altmetric Badge
    Chapter 55 Combining symbolic computation and theorem proving: Some problems of Ramanujan
  57. Altmetric Badge
    Chapter 56 SCOTT: Semantically constrained otter system description
  58. Altmetric Badge
    Chapter 57 Protein: A PRO ver with a T heory E xtension IN terface
  59. Altmetric Badge
    Chapter 58 DELTA — A bottom-up preprocessor for top-down theorem provers
  60. Altmetric Badge
    Chapter 59 SETHEO V3.2: Recent developments
  61. Altmetric Badge
    Chapter 60 KoMeT
  62. Altmetric Badge
    Chapter 61 Ω-MKRP: A proof development environment
  63. Altmetric Badge
    Chapter 62 Lean T A P : Lean tableau-based theorem proving
  64. Altmetric Badge
    Chapter 63 FINDER: Finite domain enumerator system description
  65. Altmetric Badge
    Chapter 64 Symlog automated advice in Fitch-style proof construction
  66. Altmetric Badge
    Chapter 65 KEIM: A toolkit for automated deduction
  67. Altmetric Badge
    Chapter 66 Elf: A meta-language for deductive systems
  68. Altmetric Badge
    Chapter 67 EUODHILOS-II on top of GNU epoch
  69. Altmetric Badge
    Chapter 68 Pi: An interactive derivation editor for the calculus of partial inductive definitions
  70. Altmetric Badge
    Chapter 69 Mollusc a general proof-development shell for sequent-based logics
  71. Altmetric Badge
    Chapter 70 KITP-93: An automated inference system for program analysis
  72. Altmetric Badge
    Chapter 71 SPIKE: A system for sufficient completeness and parameterized inductive proofs
  73. Altmetric Badge
    Chapter 72 Distributed theorem proving by Peers
Attention for Chapter 32: Ordered chaining for total orderings
Altmetric Badge

Citations

dimensions_citation
10 Dimensions
You are seeing a free-to-access but limited selection of the activity Altmetric has collected about this research output. Click here to find out more.
Chapter title
Ordered chaining for total orderings
Chapter number 32
Book title
Automated Deduction — CADE-12
Published by
Springer, Berlin, Heidelberg, June 1994
DOI 10.1007/3-540-58156-1_32
Book ISBNs
978-3-54-058156-7, 978-3-54-048467-7
Authors

Leo Bachmair, Harald Ganzinger, Bachmair, Leo, Ganzinger, Harald