The Resource Automated deduction-CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings, Andrei Voronkov, ed

Automated deduction-CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings, Andrei Voronkov, ed

Label
Automated deduction-CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings
Title
Automated deduction-CADE-18
Title remainder
18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings
Statement of responsibility
Andrei Voronkov, ed
Creator
Contributor
Subject
Genre
Language
eng
Member of
Cataloging source
DLC
Illustrations
illustrations
Index
no index present
LC call number
QA76.9.A96
LC item number
I57 2002
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2002
http://bibfra.me/vocab/lite/meetingName
International Conference on Automated Deduction
http://library.link/vocab/relatedWorkOrContributorDate
1959-
http://library.link/vocab/relatedWorkOrContributorName
Voronkov, Andrei
Series statement
  • Lecture notes in computer science,
  • Lecture notes in artificial intelligence
Series volume
2392.
http://library.link/vocab/subjectName
  • Automatic theorem proving
  • Logic, Symbolic and mathematical
  • processus décision
  • théorie modèle
  • résolution
  • théorie type
  • vérification modèle
  • vérification formelle
  • démonstrateur théorème
  • raisonnement automatique
  • théorie preuve
  • déduction automatique
  • Logique symbolique et mathématique
  • Théorèmes
  • Automatic theorem proving
  • Logic, Symbolic and mathematical
  • Automatische bewijsvoering
  • Théorèmes
Label
Automated deduction-CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings, Andrei Voronkov, ed
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
volume
Carrier category code
  • nc
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
Reasoning with Expressive Description Logics: Theory and Practice / Ian Horrocks -- BDD-Based Decision Procedures for K / Guoqiang Pan, Ulrike Sattler and Moshe Y. Vardi -- Temporal Logic for Proof-Carrying Code / Andrew Bernard and Peter Lee -- A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code / Robert R. Schneck and George C. Necula -- Formal Verification of a Java Compiler in Isabelle / Martin Strecker -- Embedding Lax Logic into Intuitionistic Logic / Uwe Egly -- Combining Proof-Search and Counter-Model Construction for Deciding Godel-Dummett Logic / Dominique Larchey-Wendling -- Connection-Based Proof Search in Propositional BI Logic / Didier Galmiche and Daniel Mery -- DDDLIB: A Library for Solving Quantified Difference Inequalities / Jesper B. Moller -- An LCF-Style Interface between HOL and First-Order Logic / Joe Hurd -- System Description: The Math Web Software Bus for Distributed Mathematical Reasoning / Jurgen Zimmer and Michael Kohlhase -- Proof Development with [Omega]MEGA / Jorg Siekmann, Christoph Benzmuller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth and Jurgen Zimmer -- Learn[Omega]matic: System Description / Mateja Jamnik, Manfred Kerber and Martin Pollet -- HyLoRes 1.0: Direct Resolution for Hybrid Logics / Carlos Areces and Juan Heguiabehere -- Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points / Eugene Goldberg -- A Note on Symmetry Heuristics in SEM / Thierry Boy de la Tour -- A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions / Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz and Roberto Sebastiani -- Deductive Search for Errors in Free Data Type Specifications Using Model Generation / Wolfgang Ahrendt -- Reasoning by Symmetry and Function Ordering in Finite Model Generation / Gilles Audemard and Belaid Benhamou -- Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations / Bernhard Gramlich and Reinhard Pichler -- A New Clausal Class Decidable by Hyperresolution / Lilia Georgieva, Ullrich Hustadt and Renate A. Schmidt -- Spass Version 2.0 / Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobald and Dalibor Topic -- System Description: GrAnDe 1.0 / Stephan Schulz and Geoff Sutcliffe -- The HR Program for Theorem Generation / Simon Colton -- AutoBayes/CC -- Combining Program Synthesis with Automatic Code Certification -- System Description / Michael Whalen, Johann Schumann and Bernd Fischer -- The Quest for Efficient Boolean Satisfiability Solvers / Lintao Zhang and Sharad Malik -- Recursive Path Orderings Can Be Context-Sensitive / Cristina Borralleras, Salvador Lucas and Albert Rubio -- Shostak Light / Harald Ganzinger -- Formal Verification of a Combination Decision Procedure / Jonathan Ford and Natarajan Shankar -- Combining Multisets with Integers / Calogero G. Zarba -- The Reflection Theorem: A Study in Meta-theoretic Reasoning / Lawrence C. Paulson -- Faster Proof Checking in the Edinburgh Logical Framework / Aaron Stump and David L. Dill -- Solving for Set Variables in Higher-Order Theorem Proving / Chad E. Brown -- The Complexity of the Graded [mu]-Calculus / Orna Kupferman, Ulrike Sattler and Moshe Y. Vardi -- Lazy Theorem Proving for Bounded Model Checking over Infinite Domains / Leonardo de Moura, Harald Ruess and Maria Sorea -- Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation / Miquel Bofill and Albert Rubio -- Basic Syntactic Mutation / Christopher Lynch and Barbara Morawska -- The Next Waldmeister Loop / Thomas Hillenbrand and Bernd Lochner -- Focussing Proof-Net Construction as a Middleware Paradigm / Jean Marc Andreoli -- Proof Analysis by Resolution / Matthias Baaz
Dimensions
25 cm.
Dimensions
unknown
Extent
xii, 534 pages
Isbn
9783540439318
Isbn Type
(pbk. : alk paper)
Lccn
2002026687
Media category
unmediated
Media MARC source
rdamedia
Media type code
  • n
Other physical details
illustrations
Specific material designation
remote
System control number
  • (OCoLC)50072158
  • (OCoLC)ocm50072158
Label
Automated deduction-CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings, Andrei Voronkov, ed
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
volume
Carrier category code
  • nc
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
Reasoning with Expressive Description Logics: Theory and Practice / Ian Horrocks -- BDD-Based Decision Procedures for K / Guoqiang Pan, Ulrike Sattler and Moshe Y. Vardi -- Temporal Logic for Proof-Carrying Code / Andrew Bernard and Peter Lee -- A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code / Robert R. Schneck and George C. Necula -- Formal Verification of a Java Compiler in Isabelle / Martin Strecker -- Embedding Lax Logic into Intuitionistic Logic / Uwe Egly -- Combining Proof-Search and Counter-Model Construction for Deciding Godel-Dummett Logic / Dominique Larchey-Wendling -- Connection-Based Proof Search in Propositional BI Logic / Didier Galmiche and Daniel Mery -- DDDLIB: A Library for Solving Quantified Difference Inequalities / Jesper B. Moller -- An LCF-Style Interface between HOL and First-Order Logic / Joe Hurd -- System Description: The Math Web Software Bus for Distributed Mathematical Reasoning / Jurgen Zimmer and Michael Kohlhase -- Proof Development with [Omega]MEGA / Jorg Siekmann, Christoph Benzmuller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth and Jurgen Zimmer -- Learn[Omega]matic: System Description / Mateja Jamnik, Manfred Kerber and Martin Pollet -- HyLoRes 1.0: Direct Resolution for Hybrid Logics / Carlos Areces and Juan Heguiabehere -- Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points / Eugene Goldberg -- A Note on Symmetry Heuristics in SEM / Thierry Boy de la Tour -- A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions / Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz and Roberto Sebastiani -- Deductive Search for Errors in Free Data Type Specifications Using Model Generation / Wolfgang Ahrendt -- Reasoning by Symmetry and Function Ordering in Finite Model Generation / Gilles Audemard and Belaid Benhamou -- Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations / Bernhard Gramlich and Reinhard Pichler -- A New Clausal Class Decidable by Hyperresolution / Lilia Georgieva, Ullrich Hustadt and Renate A. Schmidt -- Spass Version 2.0 / Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobald and Dalibor Topic -- System Description: GrAnDe 1.0 / Stephan Schulz and Geoff Sutcliffe -- The HR Program for Theorem Generation / Simon Colton -- AutoBayes/CC -- Combining Program Synthesis with Automatic Code Certification -- System Description / Michael Whalen, Johann Schumann and Bernd Fischer -- The Quest for Efficient Boolean Satisfiability Solvers / Lintao Zhang and Sharad Malik -- Recursive Path Orderings Can Be Context-Sensitive / Cristina Borralleras, Salvador Lucas and Albert Rubio -- Shostak Light / Harald Ganzinger -- Formal Verification of a Combination Decision Procedure / Jonathan Ford and Natarajan Shankar -- Combining Multisets with Integers / Calogero G. Zarba -- The Reflection Theorem: A Study in Meta-theoretic Reasoning / Lawrence C. Paulson -- Faster Proof Checking in the Edinburgh Logical Framework / Aaron Stump and David L. Dill -- Solving for Set Variables in Higher-Order Theorem Proving / Chad E. Brown -- The Complexity of the Graded [mu]-Calculus / Orna Kupferman, Ulrike Sattler and Moshe Y. Vardi -- Lazy Theorem Proving for Bounded Model Checking over Infinite Domains / Leonardo de Moura, Harald Ruess and Maria Sorea -- Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation / Miquel Bofill and Albert Rubio -- Basic Syntactic Mutation / Christopher Lynch and Barbara Morawska -- The Next Waldmeister Loop / Thomas Hillenbrand and Bernd Lochner -- Focussing Proof-Net Construction as a Middleware Paradigm / Jean Marc Andreoli -- Proof Analysis by Resolution / Matthias Baaz
Dimensions
25 cm.
Dimensions
unknown
Extent
xii, 534 pages
Isbn
9783540439318
Isbn Type
(pbk. : alk paper)
Lccn
2002026687
Media category
unmediated
Media MARC source
rdamedia
Media type code
  • n
Other physical details
illustrations
Specific material designation
remote
System control number
  • (OCoLC)50072158
  • (OCoLC)ocm50072158

Library Locations

  • African Studies LibraryBorrow it
    771 Commonwealth Avenue, 6th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Alumni Medical LibraryBorrow it
    72 East Concord Street, Boston, MA, 02118, US
    42.336388 -71.072393
  • Astronomy LibraryBorrow it
    725 Commonwealth Avenue, 6th Floor, Boston, MA, 02445, US
    42.350259 -71.105717
  • Fineman and Pappas Law LibrariesBorrow it
    765 Commonwealth Avenue, Boston, MA, 02215, US
    42.350979 -71.107023
  • Frederick S. Pardee Management LibraryBorrow it
    595 Commonwealth Avenue, Boston, MA, 02215, US
    42.349626 -71.099547
  • Howard Gotlieb Archival Research CenterBorrow it
    771 Commonwealth Avenue, 5th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Mugar Memorial LibraryBorrow it
    771 Commonwealth Avenue, Boston, MA, 02215, US
    42.350723 -71.108227
  • Music LibraryBorrow it
    771 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Pikering Educational Resources LibraryBorrow it
    2 Silber Way, Boston, MA, 02215, US
    42.349804 -71.101425
  • School of Theology LibraryBorrow it
    745 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350494 -71.107235
  • Science & Engineering LibraryBorrow it
    38 Cummington Mall, Boston, MA, 02215, US
    42.348472 -71.102257
  • Stone Science LibraryBorrow it
    675 Commonwealth Avenue, Boston, MA, 02445, US
    42.350103 -71.103784
Processing Feedback ...