Automated deduction--CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999 : proceedings
著者
書誌事項
Automated deduction--CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999 : proceedings
(Lecture notes in computer science, 1632 . Lecture notes in artificial intelligence)
Springer, c1999
大学図書館所蔵 全43件
  青森
  岩手
  宮城
  秋田
  山形
  福島
  茨城
  栃木
  群馬
  埼玉
  千葉
  東京
  神奈川
  新潟
  富山
  石川
  福井
  山梨
  長野
  岐阜
  静岡
  愛知
  三重
  滋賀
  京都
  大阪
  兵庫
  奈良
  和歌山
  鳥取
  島根
  岡山
  広島
  山口
  徳島
  香川
  愛媛
  高知
  福岡
  佐賀
  長崎
  熊本
  大分
  宮崎
  鹿児島
  沖縄
  韓国
  中国
  タイ
  イギリス
  ドイツ
  スイス
  フランス
  ベルギー
  オランダ
  スウェーデン
  ノルウェー
  アメリカ
注記
Includes bibliographical references and index
内容説明・目次
内容説明
This volume contains the papers presented at the Sixteenth International Conference on Automated Deduction (CADE-16), held in Trento, Italy, July 7{10, 1999, and hosted by Istituto Trentino di Cultura { Centro per la ricerca scientic a e tecnologica (ITC-IRST). The year 1999 marks the 25th anniv- sary of CADE. Since their inception in 1974 at Argonne National Laboratory, the CADE conferences have matured into the major forum for presentation of research in all aspects of automated deduction. CADE-16 was one of the conferences participating in the 1999 Federated LogicConference (FLoC). FLoC'99was the second Federated LogicConference; the r st took place in 1996 and was hosted by DIMACS at Rutgers University, NewBrunswick, NJ.TheintentionoftheFederatedLogicConferences istobring together as a synergetic group several conferences that apply logic to computer science. Theother participatingconferences in FLoC'99were theEleventh Int- national Conference on Computer-Aided Veri cation (CAV'99), the Fourteenth IEEE Symposium on Logic inComputer Science (LICS'99), and the Tenth C- ference on Rewriting Techniques and Applications (RTA-99).
Eighty-three papers were submitted to CADE-16: 67 regular papers and 16 system descriptions. Each of the submissions was reviewed by at least four programcommitteemembers, andanelectronicprogramcommitteemeeting was held through the Internet. Of the 83 papers, 21 regular papers and 15 system descriptions were accepted. In addition, this volume contains full papers by two of the four invited speakers, Erich Gr. adel and Robert Nieuwenhuis, along with an abstract of Tobias Nipkow's invited lecture. Zohar Manna gave an invited talk in a plenary session with CAV.
目次
Session 1.- A Dynamic Programming Approach to Categorial Deduction.- Tractable Transformations from Modal Provability Logics into First-Order Logic.- Session 2.- Decision Procedures for Guarded Logics.- A PSpace Algorithm for Graded Modal Logic.- Session 3.- Solvability of Context Equations with Two Context Variables Is Decidable.- Complexity of the Higher Order Matching.- Solving Equational Problems Efficiently.- Session 4.- VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up.- A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers.- Presenting Proofs in a Human-Oriented Way.- Session 5.- On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results.- Maslov's Class K Revisited.- Prefixed Resolution: A Resolution Method for Modal and Description Logics.- Session 6: System Descriptions.- System Description: Twelf - A Meta-Logical Framework for Deductive Systems.- System Description: inka 5.0 - A Logic Voyager.- System Description: CutRes 0.1: Cut Elimination by Resolution.- System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving.- System Description Using OBDD's for the Validationof Skolem Verification Conditions.- Fault-Tolerant Distributed Theorem Proving.- System Description: Waldmeister - Improvements in Performance and Ease of Use.- Session 7.- Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems.- A Formalization of Static Analyses in System F.- On Explicit Reflection in Theorem Proving and Formal Verification.- Session 8: System Descriptions.- System Description: Kimba, A Model Generator for Many-Valued First-Order Logics.- System Description: Teyjus-A Compiler and Abstract Machine Based Implementation of ?Prolog.- Vampire.- System Abstract: E 0.3.- Session 9.- Invited Talk: Rewrite-Based Deduction and Symbolic Constraints.- Towards an Automatic Analysis of Security Protocols in First-Order Logic.- Session 10.- A Confluent Connection Calculus.- Abstraction-Based Relevancy Testing for Model Elimination.- A Breadth-First Strategy for Mating Search.- Session 11: System Competitions.- The Design of the CADE-16 Inductive Theorem Prover Contest.- Session 12: System Descriptions.- System Description: Spass Version 1.0.0.- K : A Theorem Prover for K.- System Description: CYNTHIA.- System Description: MCS: Model-Based Conjecture Searching.- Session 13.- Embedding Programming Languages in Theorem Provers.- Extensional Higher-Order Paramodulation and RUE-Resolution.- Automatic Generation of Proof Search Strategies for Second-Order Logic.
「Nielsen BookData」 より