Automated deduction : a basis for applications
著者
書誌事項
Automated deduction : a basis for applications
(Applied logic series, v.8-10)
Kluwer Academic, c1998
- set
- v.1
- v.2
- v.3
大学図書館所蔵 件 / 全21件
-
v.1410.1||B-12||16021248,
v.2410.1||B-12||26021249, v.3410.1||B-12||36021250 -
v.1C||Automated-1||198032517,
v.2C||Automated-1||298032518, v.3C||Automated-1||398032519 -
v.1116-0-14//8030009808908,
v.2116-0-14//9030009808909, v.3116-0-14//10030009808910 -
v.1410.9||1||27311103143,
v.2410.9||2||27311103144, v.3410.9||3||27311103145 -
該当する所蔵館はありません
- すべての絞り込み条件を解除する
注記
Includes bibliographies and indexes
収録内容
- v.1. Foundations. calculi and methods
- v.2. Systems and implementation techniques
- v.3. Applications
内容説明・目次
- 巻冊次
-
v.1 ISBN 9780792351290
内容説明
目次
- Volume I: Foundations. Calculi and Methods. Preface
- W. Bibel, P.H. Schmitt. Part One: Tableau and Connection Calculi. Introduction
- U. Furbach. 1. Analytic Tableaux
- B. Beckert, R. Hahnle. 2. Clausal Tableaux
- R. Letz. 3. Variants of Clausal Tableaux
- P. Baumgartner, U. Furbach. 4. Cuts in Tableaux
- U. Egly. 5. Compressions and Extensions
- W. Bibel, et al. Part Two: Special Calculi and Refinements. Introduction
- U. Petermann. 6. Theory Reasoning
- P. Baumgartner, U. Petermann. 7. Unification Theory
- F. Baader, K.U. Schulz. 8. Rigid E-Unification
- B. Beckert. 9. Sorted Unification and Tree Automata
- C. Weidenbach. 10. Dimensions of Types in Logic Programming
- G. Meyer, C. Beierle. 11. Equational Reasoning in Saturation-Based Theorem Proving
- L. Bachmair, H. Ganzinger. 12. Higher-Order Rewriting and Equational Reasoning
- T. Nipkow, C. Prehofer. 13. Higher-Order Automated Theorem Proving
- M. Kohlhase. Index. Volume II: Systems and Implementation Techniques. Introduction
- T. Nipkow, W. Reif. 1. Structured Specifications and Interactive Proofs with KIV
- W. Reif, et al. 2. Proof Theory at Work: Program Development in the Minlog System
- H. Benl, et al. 3. Interactive and Automated Proof Construction in Type Theory
- M. Strecker, et al. 4. Integrating Automated and Interactive Theorem Proving
- W. Ahrendt, et al. Part Two: Representation and Optimization Techniques. Introduction
- J. Siekmann, D. Fehrer. 5. Term Indexing
- P. Graf, D. Fehrer. 6. Developing Deduction Systems: The Toolbox Style
- D. Fehrer. 7. Specifications of Inference Rules: Extensions of the PTTP Technique
- G. Neugebauer, U. Petermann. 8. Proof Analysis, Generalization and Reuse
- T. Kolbe, C. Walther. Part Three: Parallel Inference Systems. Introduction
- W. Kuchlin. 9. Parallel Term Rewriting with PaReDuX
- R. Bundgen, et al. 10. Parallel Theorem Provers Based on SETHEO
- J. Schumann, et al. 11. Massively Parallel Reasoning
- S.-E. Bornscheuer, et al. Part Four: Comparison and Cooperation of Theorem Provers. Introduction
- J. Avenhaus. 12. Extension Methods in Automated Deduction
- M. Baaz, et al. 13. A Comparison of Equality Reasoning Heuristics
- J. Denzinger, M. Fuchs. 14. Cooperating Theorem Provers
- J. Denzinger, I. Dahn. Index. Volume III: Applications. Part One: Automated Theorem Proving in Mathematics. Introduction
- M. Kohlhase. 1. Lattice-Ordered Groups in Deduction
- I. Dahn. 2. Superposition Theorem Proving for Commutative Rings
- J. Stuber. 3. How to Augment a Formal System with a Boolean Algebra Component
- H.J. Ohlbach, J. Kuhler. 4. Proof Planning: A practical Approach to Mechanized Reasoning in Mathematics
- M. Kerber. Part Two: Automated Deduction in Software Engineering and hardware Design. Introduction
- J. Schumann. 5. Program Synthesis
- C. Kreitz. 6. Termination Analysis for Functional Programs
- J. Giesl, et al. 7. The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV
- G. Schellhorn, W. Ahrendt. 8. Using Automated Theorem Provers in Verification of Protocols
- I. Dahn, J. Schumann. 9. Theorem Proving in Large Theories
- W. Reif, G. Schellhorn. 10. Analyzing Rule Sets for the Calculation of Banking Fees by a Theorem Prover with Constraints
- F. Stolzenburg, B. Thomas. 11. Deduction-Based Software Component Retrieval
- B. Fischer, et al. 12. Rewrite Based hardware Verification with ReDuX
- R. Bundgen. Index.
- 巻冊次
-
v.2 ISBN 9780792351306
内容説明
目次
- Volume I: Foundations. Calculi and Methods. Preface
- W. Bibel, P.H. Schmitt. Part One: Tableau and Connection Calculi. Introduction
- U. Furbach. 1. Analytic Tableaux
- B. Beckert, R. Hahnle. 2. Clausal Tableaux
- R. Letz. 3. Variants of Clausal Tableaux
- P. Baumgartner, U. Furbach. 4. Cuts in Tableaux
- U. Egly. 5. Compressions and Extensions
- W. Bibel, et al. Part Two: Special Calculi and Refinements. Introduction
- U. Petermann. 6. Theory Reasoning
- P. Baumgartner, U. Petermann. 7. Unification Theory
- F. Baader, K.U. Schulz. 8. Rigid E-Unification
- B. Beckert. 9. Sorted Unification and Tree Automata
- C. Weidenbach. 10. Dimensions of Types in Logic Programming
- G. Meyer, C. Beierle. 11. Equational Reasoning in Saturation-Based Theorem Proving
- L. Bachmair, H. Ganzinger. 12. Higher-Order Rewriting and Equational Reasoning
- T. Nipkow, C. Prehofer. 13. Higher-Order Automated Theorem Proving
- M. Kohlhase. Index. Volume II: Systems and Implementation Techniques. Introduction
- T. Nipkow, W. Reif. 1. Structured Specifications and Interactive Proofs with KIV
- W. Reif, et al. 2. Proof Theory at Work: Program Development in the Minlog System
- H. Benl, et al. 3. Interactive and Automated Proof Construction in Type Theory
- M. Strecker, et al. 4. Integrating Automated and Interactive Theorem Proving
- W. Ahrendt, et al. PartTwo: Representation and Optimization Techniques. Introduction
- J. Siekmann, D. Fehrer. 5. Term Indexing
- P. Graf, D. Fehrer. 6. Developing Deduction Systems: The Toolbox Style
- D. Fehrer. 7. Specifications of Inference Rules: Extensions of the PTTP Technique
- G. Neugebauer, U. Petermann. 8. Proof Analysis, Generalization and Reuse
- T. Kolbe, C. Walther. Part Three: Parallel Inference Systems. Introduction
- W. Kuchlin. 9. Parallel Term Rewriting with PaReDuX
- R. Bundgen, et al. 10. Parallel Theorem Provers Based on SETHEO
- J. Schumann, et al. 11. Massively Parallel Reasoning
- S.-E. Bornscheuer, et al. Part Four: Comparison and Cooperation of Theorem Provers. Introduction
- J. Avenhaus. 12. Extension Methods in Automated Deduction
- M. Baaz, et al. 13. A Comparison of Equality Reasoning Heuristics
- J. Denzinger, M. Fuchs. 14. Cooperating Theorem Provers
- J. Denzinger, I. Dahn. Index. Volume III: Applications. Part One: Automated Theorem Proving in Mathematics. Introduction
- M. Kohlhase. 1. Lattice-Ordered Groups in Deduction
- I. Dahn. 2. Superposition Theorem Proving for Commutative Rings
- J. Stuber. 3. How to Augment a Formal System with a Boolean Algebra Component
- H.J. Ohlbach, J. Kuhler. 4. Proof Planning: A practical Approach to Mechanized Reasoning in Mathematics
- M. Kerber. Part Two: Automated Deduction in Software Engineering and hardware Design. Introduction
- J. Schum
- 巻冊次
-
v.3 ISBN 9780792351313
内容説明
目次
- Volume I: Foundations. Calculi and Methods. Preface
- W. Bibel, P.H. Schmitt. Part One: Tableau and Connection Calculi. Introduction
- U. Furbach. 1. Analytic Tableaux
- B. Beckert, R. Hahnle. 2. Clausal Tableaux
- R. Letz. 3. Variants of Clausal Tableaux
- P. Baumgartner, U. Furbach. 4. Cuts in Tableaux
- U. Egly. 5. Compressions and Extensions
- W. Bibel, et al. Part Two: Special Calculi and Refinements. Introduction
- U. Petermann. 6. Theory Reasoning
- P. Baumgartner, U. Petermann. 7. Unification Theory
- F. Baader, K.U. Schulz. 8. Rigid E-Unification
- B. Beckert. 9. Sorted Unification and Tree Automata
- C. Weidenbach. 10. Dimensions of Types in Logic Programming
- G. Meyer, C. Beierle. 11. Equational Reasoning in Saturation-Based Theorem Proving
- L. Bachmair, H. Ganzinger. 12. Higher-Order Rewriting and Equational Reasoning
- T. Nipkow, C. Prehofer. 13. Higher-Order Automated Theorem Proving
- M. Kohlhase. Index. Volume II: Systems and Implementation Techniques. Introduction
- T. Nipkow, W. Reif. 1. Structured Specifications and Interactive Proofs with KIV
- W. Reif, et al. 2. Proof Theory at Work: Program Development in the Minlog System
- H. Benl, et al. 3. Interactive and Automated Proof Construction in Type Theory
- M. Strecker, et al. 4. Integrating Automated and Interactive Theorem Proving
- W. Ahrendt, et al. PartTwo: Representation and Optimization Techniques. Introduction
- J. Siekmann, D. Fehrer. 5. Term Indexing
- P. Graf, D. Fehrer. 6. Developing Deduction Systems: The Toolbox Style
- D. Fehrer. 7. Specifications of Inference Rules: Extensions of the PTTP Technique
- G. Neugebauer, U. Petermann. 8. Proof Analysis, Generalization and Reuse
- T. Kolbe, C. Walther. Part Three: Parallel Inference Systems. Introduction
- W. Kuchlin. 9. Parallel Term Rewriting with PaReDuX
- R. Bundgen, et al. 10. Parallel Theorem Provers Based on SETHEO
- J. Schumann, et al. 11. Massively Parallel Reasoning
- S.-E. Bornscheuer, et al. Part Four: Comparison and Cooperation of Theorem Provers. Introduction
- J. Avenhaus. 12. Extension Methods in Automated Deduction
- M. Baaz, et al. 13. A Comparison of Equality Reasoning Heuristics
- J. Denzinger, M. Fuchs. 14. Cooperating Theorem Provers
- J. Denzinger, I. Dahn. Index. Volume III: Applications. Part One: Automated Theorem Proving in Mathematics. Introduction
- M. Kohlhase. 1. Lattice-Ordered Groups in Deduction
- I. Dahn. 2. Superposition Theorem Proving for Commutative Rings
- J. Stuber. 3. How to Augment a Formal System with a Boolean Algebra Component
- H.J. Ohlbach, J. Kuhler. 4. Proof Planning: A practical Approach to Mechanized Reasoning in Mathematics
- M. Kerber. Part Two: Automated Deduction in Software Engineering and hardware Design. Introduction
- J. Schum
- 巻冊次
-
set ISBN 9780792351320
内容説明
目次
- Volume I: Foundations. Calculi and Methods. Preface
- W. Bibel, P.H. Schmitt. Part One: Tableau and Connection Calculi. Introduction
- U. Furbach. 1. Analytic Tableaux
- B. Beckert, R. Hahnle. 2. Clausal Tableaux
- R. Letz. 3. Variants of Clausal Tableaux
- P. Baumgartner, U. Furbach. 4. Cuts in Tableaux
- U. Egly. 5. Compressions and Extensions
- W. Bibel, et al. Part Two: Special Calculi and Refinements. Introduction
- U. Petermann. 6. Theory Reasoning
- P. Baumgartner, U. Petermann. 7. Unification Theory
- F. Baader, K.U. Schulz. 8. Rigid E-Unification
- B. Beckert. 9. Sorted Unification and Tree Automata
- C. Weidenbach. 10. Dimensions of Types in Logic Programming
- G. Meyer, C. Beierle. 11. Equational Reasoning in Saturation-Based Theorem Proving
- L. Bachmair, H. Ganzinger. 12. Higher-Order Rewriting and Equational Reasoning
- T. Nipkow, C. Prehofer. 13. Higher-Order Automated Theorem Proving
- M. Kohlhase. Index. Volume II: Systems and Implementation Techniques. Introduction
- T. Nipkow, W. Reif. 1. Structured Specifications and Interactive Proofs with KIV
- W. Reif, et al. 2. Proof Theory at Work: Program Development in the Minlog System
- H. Benl, et al. 3. Interactive and Automated Proof Construction in Type Theory
- M. Strecker, et al. 4. Integrating Automated and Interactive Theorem Proving
- W. Ahrendt, et al. Part Two: Representation and Optimization Techniques. Introduction
- J. Siekmann, D. Fehrer. 5. Term Indexing
- P. Graf, D. Fehrer. 6. Developing Deduction Systems: The Toolbox Style
- D. Fehrer. 7. Specifications of Inference Rules: Extensions of the PTTP Technique
- G. Neugebauer, U. Petermann. 8. Proof Analysis, Generalization and Reuse
- T. Kolbe, C. Walther. Part Three: Parallel Inference Systems. Introduction
- W. Kuchlin. 9. Parallel Term Rewriting with PaReDuX
- R. Bundgen, et al. 10. Parallel Theorem Provers Based on SETHEO
- J. Schumann, et al. 11. Massively Parallel Reasoning
- S.-E. Bornscheuer, et al. Part Four: Comparison and Cooperation of Theorem Provers. Introduction
- J. Avenhaus. 12. Extension Methods in Automated Deduction
- M. Baaz, et al. 13. A Comparison of Equality Reasoning Heuristics
- J. Denzinger, M. Fuchs. 14. Cooperating Theorem Provers
- J. Denzinger, I. Dahn. Index. Volume III: Applications. Part One: Automated Theorem Proving in Mathematics. Introduction
- M. Kohlhase. 1. Lattice-Ordered Groups in Deduction
- I. Dahn. 2. Superposition Theorem Proving for Commutative Rings
- J. Stuber. 3. How to Augment a Formal System with a Boolean Algebra Component
- H.J. Ohlbach, J. Kuhler. 4. Proof Planning: A practical Approach to Mechanized Reasoning in Mathematics
- M. Kerber. Part Two: Automated Deduction in Software Engineering and hardware Design. Introduction
- J. Schumann. 5. Program Synthesis
- C. Kreitz. 6. Termination Analysis for Functional Programs
- J. Giesl, et al. 7. The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV
- G. Schellhorn, W. Ahrendt. 8. Using Automated Theorem Provers in Verification of Protocols
- I. Dahn, J. Schumann. 9. Theorem Proving in Large Theories
- W. Reif, G. Schellhorn. 10. Analyzing Rule Sets for the Calculation of Banking Fees by a Theorem Prover with Constraints
- F. Stolzenburg, B. Thomas. 11. Deduction-Based Software Component Retrieval
- B. Fischer, et al. 12. Rewrite Based hardware Verification with ReDuX
- R. Bundgen. Index.
「Nielsen BookData」 より