Logo - springer
Slogan - springer

Computer Science - Artificial Intelligence | Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction Nancy, France,

Automated Deduction — CADE-12

12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings

Bundy, Alan (Ed.)

1994, XVI, 852 p. In 2 volumes, not available separately.

Available Formats:

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.


ISBN 978-3-540-48467-7

digitally watermarked, no DRM

The eBook version of this title will be available soon

learn more about Springer eBooks

add to marked items


Softcover (also known as softback) version.

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.


(net) price for USA

ISBN 978-3-540-58156-7

free shipping for individuals worldwide

The book title is in reprint. You can already preorder it.

add to marked items

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.

Content Level » Research

Keywords » Automatisches Schließen - KI-Logiken - Logic Programming - Logisches Prorammieren - Term Rewriting - Term-Ersetzung - Theorem Proving - Variable - automated deduction - automated reasoning - complexity - grammar - heuristics - lambda calculus - proving

Related subjects » Artificial Intelligence - Mathematics - Theoretical Computer Science

Table of contents 

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.

Popular Content within this publication 



Read this Book on Springerlink

Services for this book

New Book Alert

Get alerted on new Springer publications in the subject area of Artificial Intelligence (incl. Robotics).