عنوان

Automated Deduction -- CADE-12 :

شابک

0387581561

شابک

3540484671

شابک

3540581561

شابک

9780387581569

شابک

9783540484677

شابک

9783540581567

شماره

b566304

عنوان اصلي

Automated Deduction -- CADE-12 :

نام عام مواد

[Book]

ساير اطلاعات عنواني

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

نام نخستين پديدآور

edited by Alan Bundy.

محل نشرو پخش و غیره

Berlin, Heidelberg

نام ناشر، پخش کننده و غيره

Springer-Verlag

تاریخ نشرو بخش و غیره

1994

نام خاص و کميت اثر

: v.: digital

عنوان فروست

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

متن يادداشت

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.

متن يادداشت

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.

موضوع مستند نشده

Artificial intelligence.

موضوع مستند نشده

Computer science.

موضوع مستند نشده

Logic, Symbolic and mathematical.

مستند نام اشخاص تاييد نشده

edited by Alan Bundy.

مستند نام اشخاص تاييد نشده

Alan Bundy

نام الکترونيکي

نوع ماده

[Book]

تكميل شده

Y