Automated Deduction - CADE-12
12th International Conference on Automated Deduction Nancy, France, June 26-July 1, 1994 Proceedings
(Sprache: Englisch)
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...
The 67 papers presented were selected from 177 submissions and document many of the most...
Voraussichtlich lieferbar in 3 Tag(en)
versandkostenfrei
Buch (Kartoniert)
53.49 €
26 DeutschlandCard Punkte
sammeln
- Lastschrift, Kreditkarte, Paypal, Rechnung
- Kostenlose Rücksendung
- Ratenzahlung möglich
Produktdetails
Produktinformationen zu „Automated Deduction - CADE-12 “
Klappentext zu „Automated Deduction - CADE-12 “
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.
Inhaltsverzeichnis zu „Automated Deduction - CADE-12 “
- 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
... mehr
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
- 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
... weniger
Bibliographische Angaben
- 1994, 1994, XVI, 852 Seiten, Maße: 15,5 x 23,5 cm, Kartoniert (TB), Englisch
- Herausgegeben: Alan Bundy
- Verlag: Springer, Berlin
- ISBN-10: 3540581561
- ISBN-13: 9783540581567
- Erscheinungsdatum: 08.06.1994
Sprache:
Englisch
Kommentar zu "Automated Deduction - CADE-12"
0 Gebrauchte Artikel zu „Automated Deduction - CADE-12“
| Zustand | Preis | Porto | Zahlung | Verkäufer | Rating |
|---|
Schreiben Sie einen Kommentar zu "Automated Deduction - CADE-12".
Kommentar verfassen