1994, XVI, 852 p. In 2 volumes, not available separately.
Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.
You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.
After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.
digitally watermarked, no DRM
The eBook version of this title will be available soon
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.
The crisis in finite mathematics: Automated reasoning as cause and cure.- A divergence critic.- Synthesis of induction orderings for existence proofs.- Lazy generation of induction hypotheses.- The search efficiency of theorem proving strategies.- A method for building models automatically. Experiments with an extension of OTTER.- Model elimination without contrapositives.- Induction using term orderings.- Mechanizable inductive proofs for a class of ? ? formulas.- On the connection between narrowing and proof by consistency.- A fixedpoint approach to implementing (Co)inductive definitions.- On notions of inductive validity for first-order equational clauses.- A new application for explanation-based generalisation within automated deduction.- Semantically guided first-order theorem proving using hyper-linking.- The applicability of logic program analysis and transformation to theorem proving.- Detecting non-provable goals.- A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?.- The TPTP problem library.- Combination techniques for non-disjoint equational theories.- Primal grammars and unification modulo a binary clause.- Conservative query normalization on parallel circumscription.- Bottom-up evaluation of Datalog programs with arithmetic constraints.- On intuitionistic query answering in description bases.- Deductive composition of astronomical software from subroutine libraries.- Proof script pragmatics in IMPS.- A mechanization of strong Kleene logic for partial functions.- Algebraic factoring and geometry theorem proving.- Mechanically proving geometry theorems using a combination of Wu's method and Collins' method.- Str?ve and integers.- What is a proof?.- Termination, geometry and invariants.- Ordered chaining for total orderings.- Simple termination revisited.- Termination orderings for rippling.- A novel asynchronous parallelism scheme for first-order logic.- Proving with BDDs and control of information.- Extended path-indexing.- Exporting and reflecting abstract metamathematics.- Associative-commutative deduction with constraints.- AC-superposition with constraints: No AC-unifiers needed.- The complexity of counting problems in equational matching.- Representing proof transformations for program optimization.- Exploring abstract algebra in constructive type theory.- Tactic theorem proving with refinement-tree proofs and metavariables.- Unification in an extensional lambda calculus with ordered function sorts and constant overloading.- Decidable higher-order unification problems.- Theory and practice of minimal modular higher-order E-unification.- A refined version of general E-unification.- A completion-based method for mixed universal and rigid E-unification.- On pot, pans and pudding or how to discover generalised critical Pairs.- Semantic tableaux with ordering restrictions.- Strongly analytic tableaux for normal modal logics.- Reconstructing proofs at the assertion level.- Problems on the generation of finite models.- Combining symbolic computation and theorem proving: Some problems of Ramanujan.- SCOTT: Semantically constrained otter system description.- Protein: A PROver with a Theory Extension INterface.- DELTA — A bottom-up preprocessor for top-down theorem provers.- SETHEO V3.2: Recent developments.- KoMeT.- ?-MKRP: A proof development environment.- LeanT A P: Lean tableau-based theorem proving.- FINDER: Finite domain enumerator system description.- Symlog automated advice in Fitch-style proof construction.- KEIM: A toolkit for automated deduction.- Elf: A meta-language for deductive systems.- EUODHILOS-II on top of GNU epoch.- Pi: An interactive derivation editor for the calculus of partial inductive definitions.- Mollusc a general proof-development shell for sequent-based logics.- KITP-93: An automated inference system for program analysis.- SPIKE: A system for sufficient completeness and parameterized inductive proofs.- Distributed theorem proving by Peers.