|
" Automated Deduction -- CADE-12 : "
edited by Alan Bundy.
| Document Type
|
:
|
BL
|
| Record Number
|
:
|
746355
|
| Doc. No
|
:
|
b566304
|
| Main Entry
|
:
|
edited by Alan Bundy.
|
| Title & Author
|
:
|
Automated Deduction -- CADE-12 : : 12th International Conference on Automated Deduction Nancy, France, June 26 - July 1, 1994 Proceedings\ edited by Alan Bundy.
|
| Publication Statement
|
:
|
Berlin, Heidelberg : Springer-Verlag, 1994
|
| Series Statement
|
:
|
Lecture notes in computer science., Lecture notes in artificial intelligence.; Lecture notes in computer science, 814.
|
| Page. NO
|
:
|
: v.: digital
|
| ISBN
|
:
|
0387581561
|
|
|
:
|
: 3540484671
|
|
|
:
|
: 3540581561
|
|
|
:
|
: 9780387581569
|
|
|
:
|
: 9783540484677
|
|
|
:
|
: 9783540581567
|
| 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.
|
| Abstract
|
:
|
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.
|
| Subject
|
:
|
Artificial intelligence.
|
| Subject
|
:
|
Computer science.
|
| Subject
|
:
|
Logic, Symbolic and mathematical.
|
| Added Entry
|
:
|
Alan Bundy
|
| |