Automated deduction--CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999 : proceedings

>> Google Books

所蔵情報QRコード

Automated deduction--CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999 : proceedings / Harald Ganzinger (ed.)

資料種別:

図書

出版情報:

Berlin ; New York : Springer, c1999

形態:

xiv, 428 p. ; 24 cm

シリーズ名:

Lecture notes in computer science ; 1632 . Lecture notes in artificial intelligence <BA00009279>

著者名:

ISBN:

9783540662228 [3540662227]

書誌ID:

BA42176007

子書誌情報

フルテキスト

所蔵情報

他の版・巻

書誌詳細

注記:

Includes bibliographical references and index

主題:

Automatic theorem proving Congresses; Logic, Symbolic and mathematical Congresses

言語:

英語

目次情報:

A Dynamic Programming Approach to Categorial Deduction / Philippe de GrooteSession 1：

Tractable Transformations from Modal Provability Logics into First-Order Logic / Stéphane Demri ; Rajeev Goré

Invited Talk: Decision Procedures for Guarded Logics / Erich GrädelSession 2：

A PSpace Algorithm for Graded Modal Logic / Stephan Tobies

Solvability of Context Equations with Two Context Variables Is Decidable / Manfred Schmidt-Schauß ; Klaus U. SchulzSession 3：

Complexity of the Higher Order Matching / ToMasz Wierzbicki

Solving Equational Problems Efficiently / Reinhard Pichler

VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up / A. A. Adams ; H. Gottliebsen ; S. A. Linton ; U. MartinSession 4：

A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers / Predrag Janičić ; Alan Bundy ; Ian Green

Presenting Proofs in a Human-Oriented Way / Helmut Horacek

On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results / Viorica Sofronie-StokkermansSession 5：

Maslov's Class K Revisited / Ullrich Hustadt ; Renate A. Schmidt

Prefixed Resolution: A Resolution Method for Modal and Description Logics / Carlos Areces ; Hans de Nivelle ; Maarten de Rijke

System Descriptions / Session 6：

System Description: Twelf - A Meta-Logical Framework for Deductive Systems / Frank Pfenning ; Carsten Schürmann

System Description: inka 5.0 - A Logic Voyager / Serge Autexier ; Dieter Hutter ; Heiko Mantel ; Axel Schairer

System Description: CutRes 0.1: Cut Elimination by Resolution / Matthias Baaz ; Alexander Leitsch ; Georg Moser

System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving / Andreas Franke ; Michael Kohlhase

System Description: Using OBDD's for the Validation of Skolem Verification Conditions / E. Pascal Gribomont ; Nachaat Salloum

Fault-Tolerant Distributed Theorem Proving / Jason Hickey

System Description: Waldmeister - Improvements in Performance and Ease of Use / Thomas Hillenbrand ; Andreas Jaeger ; Bernd Löchner

Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems / Amy P. Felty ; Douglas J. Howe ; Abhik RoychoudhurySession 7：

A Formalization of Static Analyses in SystemF / Frédéric Prost

On Explicit Reflection in Theorem Proving and Formal Verification / Sergei N. Artemov

System Description: Kimba, A Model Generator for Many-Valued First-Order Logics / Karsten Konrad ; D. A. WolframSession 8：

System Description: Teyjus-A Compiler and Abstract Machine Based Implementation of λProlog / Gopalan Nadathur ; Dustin J. Mitchell

Vampire / Alexandre Riazanov ; Andrei Voronkov

System Abstract: E 0.3 / Stephan Schulz

Invited Talk: Rewrite-Based Deduction and Symbolic Constraints / Robert NieuwenhuisSession 9：

Towards an Automatic Analysis of Security Protocols in First-Order Logic / Christoph Weidenbach

A Confluent Connection Calculus / Peter Baumgartner ; Norbert Eisinger ; Ulrich FurbachSession 10：

Abstraction-Based Relevancy Testing for Model Elimination / Marc Fuchs ; Dirk Fuchs

A Breadth-First Strategy for Mating Search / Matthew Bishop

System Competitions / Session 11：

The Design of the CADE-16 Inductive Theorem Prover Contest

System Description: Spass Version 1.0.0 / Bijan Afshordel ; Uwe Brahm ; Christian Cohrs ; Thorsten Engel ; Enno Keen ; Christian Theobalt ; Dalibor TopićSession 12：

KK: A Theorem Prover for K

System Description: C^YNTHIA / Jon Whittle ; Richard Boulton ; Helen Lowe

System Description: MCS: Model-Based Conjecture Searching / Jian Zhang

Invited Talk: Embedding Programming Languages in Theorem Provers / Tobias NipkowSession 13：

Extensional Higher-Order Paramodulation and RUE-Resolution / Christoph Benzmüller

Automatic Generation of Proof Search Strategies for Second-Order Logic / Raul H. C. Lopes

Author Index

A Dynamic Programming Approach to Categorial Deduction / Philippe de GrooteSession 1：

Tractable Transformations from Modal Provability Logics into First-Order Logic / Stéphane Demri ; Rajeev Goré

Invited Talk: Decision Procedures for Guarded Logics / Erich GrädelSession 2：

A PSpace Algorithm for Graded Modal Logic / Stephan Tobies

Solvability of Context Equations with Two Context Variables Is Decidable / Manfred Schmidt-Schauß ; Klaus U. SchulzSession 3：

Complexity of the Higher Order Matching / ToMasz Wierzbicki

続きを見る

東工大ブックレビュー

類似資料:

1 図書 Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX '99, Saratoga Springs, NY, USA, June 7-11, 1999 : … TABLEAUX, Murray, Neil V. Springer	7 図書 Automated deduction, CADE-14 : 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997 : proceedings International Conference on Automated Deduction, McCune, W. (William) Springer
2 電子ブック Automated Deduction — CADE-16 International Conference on Automated Deduction, Ganzinger, Harald SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg	8 図書 Automated deduction -- CADE-13 : 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996 : proceedings International Conference on Automated Deduction, McRobbie, M. A. (Michael A.), Slaney, John K. Springer
3 図書 Logic for programming and automated reasoning : 6th International Conference, LPAR '99, Tbilisi, Georgia, September 6-10, 1999 : proceedings LPAR, Ganzinger, Harald, 1950-, McAllester, David A., Voronkov, A. (Andreĭ), 1959- Springer-Verlag	9 図書 Automated deduction, CADE-12 : 12th International Conference on Automated Deduction, Nancy, France, June 26-July 1, 1994 : proceedings (: us ; : gw) International Conference on Automated Deduction, Bundy, Alan Springer-Verlag
4 図書 Rewriting techniques and applications : 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996 : proceedings International Conference on Rewriting Techniques and Applications, Ganzinger, Harald, 1950- Springer-Verlag	10 図書 Automated deduction - CADE-19 : 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28-August 2, 2003 : proceedings International Conference on Automated Deduction, Baader, Franz Springer
5 電子ブック Automated Deduction - CADE 29 : 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings Pientka, Brigitte., Tinelli, Cesare SpringerLink Books - AutoHoldings, Springer International Publishing AG	11 図書 Automated deduction -- CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings International Conference on Automated Deduction, Voronkov, A. (Andreĭ), 1959- Springer
6 図書 Automated deduction - CADE-15 : 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998 : proceedings (: pbk) International Conference on Automated Deduction, Kirchner, Claude, Kirchner, Hélène Springer	12 図書 Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings International Conference on Automated Deduction, Nieuwenhuis, Robert Springer