close
1.

図書

図書
Andrei Voronkov (ed.)
出版情報: Berlin : Springer, c2002  xii, 534 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2392 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
Description Logics and Semantic Web / Session 1:
Reasoning with Expressive Description Logics: Theory and Practice / Ian Horrocks
BDD-Based Decision Procedures for <$>{\cal K}<$> / Guoqiang Pan ; Ulrike Sattler ; Moshe Y. Vardi
Proof-Carrying Code and Compiler Verification / Session 2:
Temporal Logic for Proof-Carrying Code / Andrew Bernard ; Peter Lee
A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code / Robert R. Schneck ; George C. Necula
Formal Verification of a Java Compiler in Isabelle / Martin Strecker
Non-classical Logics / Session 3:
Embedding Lax Logic into Intuitionistic Logic / Uwe Egly
Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic / Dominique Larchey-Wendling
Connection-Based Proof Search in Propositional BI Logic / Didier Galmiche ; Daniel Méry
System Descriptions / Session 4:
DDDLIB: A Library for Solving Quantified Difference Inequalities / Jesper B. Møller
An LCF-Style Interface between HOL and First-Order Logic / Joe Hurd
System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning / Jürgen Zimmer ; Michael Kohlhase
Proof Development with ΩMEGA / Jörg Siekmann ; Christoph Benzmüller ; Vladimir Brezhnev ; Lassaad Cheikhrouhou ; Armin Fiedler ; Andreas Franke ; Helmut Horacek ; Andreas Meier ; Erica Melis ; Markus Moschner ; Immanuel Normann ; Martin Pollet ; Volker Sorge ; Carsten Ullrich ; Claus-Peter Wirth ; Juörgen Zimmer
LearnΩmatic: System Description / Mateja Jamnik ; Manfred Kerber
HyLoRes 1.0: Direct Resolution for Hybrid Logics / Carlos Areces ; Juan Heguiabehere
SAT / Session 5:
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 ; Roberto Sebastiani
Model Generation / Session 6:
Deductive Search for Errors in Free Data Type Specifications Using Model Generation / Wolfgang Ahrendt
Reasoning by Symmetry and Function Ordering in Finite Model Generation / Belaid Benhamou
Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations / Bernhard Gramlich ; Reinhard Pichler
A New Clausal Class Decidable by Hyperresolution / Lilia Georgieva ; Ullrich Hustadt ; Renate A. SchmidtSession 7:
CASC / Session 8:
Spass Version 2.0 / Christoph Weidenbach ; Uwe Brahm ; Thomas Hillenbrand ; Enno Keen ; Christian Theobald ; Dalibor Topić
System Description: GrAnDe 1.0 / Stephan Schulz ; 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 ; Bernd Fischer
CADE-CAV Invited Talk
The Quest for Efficient Boolean Satisfiability Solvers / Lintao Zhang ; Sharad Malik
Recursive Path Orderings Can Be Context-Sensitive / Cristina Borralleras ; Salvador Lucas ; Albert RubioSession 9:
Combination of Decision Procedures / Session 10:
Shostak Light / Harald Ganzinger
Formal Verification of a Combination Decision Procedure / Jonathan Ford ; Natarajan Shankar
Combining Multisets with Integers / Calogero G. Zarba
Logical Frameworks / Session 11:
The Reflection Theorem: A Study in Meta-theoretic Reasoning / Lawrence C. Paulson
Faster Proof Checking in the Edinburgh Logical Framework / Aaron Stump ; David L. Dill
Solving for Set Variables in Higher-Order Theorem Proving / Chad E. Brown
Model Checking / Session 12:
The Complexity of the Graded μ-Calculus / Orna Kupferman
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains / Leonardo de Moura ; Harald Rueß ; Maria Sorea
Equational Reasoning / Session 13:
Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation / Miquel Bofill
Basic Syntactic Mutation / Christopher Lynch ; Barbara Morawska
The Next Waldmeister Loop / Bernd Lochner
Proof Theory / Session 14:
Focussing Proof-Net Construction as a Middleware Paradigm / Jean Marc Andreoli
Proof Analysis by Resolution / Matthias Baaz
Author Index
Description Logics and Semantic Web / Session 1:
Reasoning with Expressive Description Logics: Theory and Practice / Ian Horrocks
BDD-Based Decision Procedures for <$>{\cal K}<$> / Guoqiang Pan ; Ulrike Sattler ; Moshe Y. Vardi
2.

図書

図書
Claude Kirchner, Hélène Kirchner (eds.)
出版情報: Berlin : Springer, c1998  xiv, 441 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1421 . Lecture notes in artificial intelligence
所蔵情報: loading…
3.

図書

図書
David McAllester (ed.)
出版情報: Berlin : Springer, c2000  xiii, 512 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1831 . Lecture notes in artificial intelligence
所蔵情報: loading…
4.

図書

図書
Franz Baader (ed.)
出版情報: Berlin ; Tokyo : Springer, c2003  xii, 502 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2741 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
Invited Talk / Session 1:
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking / Edmund M. Clarke
Session 2
Equational Abstractions / José Meseguer ; Miguel Palomino ; Narciso Martí-Oliet
Deciding Inductive Validity of Equations / Jürgen Giesl ; Deepak Kapur
Automating the Dependency Pair Method / Nao Hirokawa ; Aart Middeldorp
An AC-Compatible Knuth-Bendix Order / Konstantin Korovin ; Andrei Voronkov
Session 3
The Complexity of Finite Model Reasoning in Description Logics / Carsten Lutz ; Ulrike Sattler ; Lidia Tendera
Optimizing a BDD-Based Modal Solver / Guoqiang Pan ; Moshe Y. Vardi
A Translation of Looping Alternating Automata into Description Logics / Jan Hladik
Session 4
Foundational Certified Code in a Metalogical Framework / Karl Crary ; Susmit Sarkar
Proving Pointer Programs in Higher-Order Logic / Farhad Mehta ; Tobias Nipkow
λ / Dimitri Hendriks ; Vincent van Oostrom
Subset Types and Partial Functions / Aaron Stump
Session 5
Reasoning about Quantifiers by Matching in the E-graphGreg Nelson
Session 6
A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols / Sumit Gulwani ; George C. Necula
Superposition Modulo a Shostak Theory / Harald Ganzinger ; Thomas Hillenbrand ; Uwe Waldmann
Canonization for Disjoint Unions of Theories / Sava Krstić ; Sylvain Conchon
Matching in a Class of Combined Non-disjoint Theories / Christophe Ringeissen
Session 7
Reasoning about Iteration in Gödel's Class Theory / Johan Gijsbertus Frederik Belinfante
Algorithms for Ordinal Arithmetic / Panagiotis Manolios ; Daron Vroon
Certifying Solutions to Permutation Group Problems / Arjeh Cohen ; Scott H. Murray ; Martin Pollet ; Volker Sorge
System Descriptions / Session 8:
TRP++ 2.0: A Temporal Resolution Prover / Ullrich Hustadt ; Boris Konev
IsaPlanner: A Prototype Proof Planner in Isabelle / Lucas Dixon ; Jacques Fleuriot
'Living Book': - 'Deduction', 'Slicing', 'Interaction' / Peter Baumgartner ; Ulrich Furbach ; Margret Gross-Hardt ; Alex Sinner
The Homer System / Simon Colton ; Sophie Huczynska
CASC-19 Results / Session 9:
The CADE-19 ATP System Competition / Geoff Sutcliffe ; Christian Suttner
Proof Search and Proof Check for Equational and Inductive Theorems / Eric Deplagne ; Claude Kirchner ; Hélène Kirchner ; Quang Huy NguyenSession 10:
The New Waldmeister Loop at Work / Jean-Marie Gaillourdet ; Bernd Löuchner ; Hendrik SpiesSession 11:
About VeriFun / Christoph Walther ; Stephan Schweitzer
How to Prove Inductive Theorems? QuodLibet! / Jürgen Avenhaus ; Ulrich Kühler ; Tobias Schmidt-Samoa ; Claus-Peter Wirth
Reasoning about Qualitative Representations of Space and Time / Anthony G. CohnSession 12:
Session 13
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation / Jürgen Stuber
The Model Evolution Calculus / Cesare Tinelli
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms / Hans de Nivelle
Efficient Instance Retrieval with Standard and Relational Path Indexing / Alexandre Riazanov
Session 14
Monodic Temporal Resolution / Anatoly Degtyarev ; Michael Fisher
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae / Renate A. Schmidt
Schematic Saturation for Decision and Unification Problems / Christopher Lynch
Session 15
Unification Modulo ACUI Plus Homomorphisms/Distributivity / Siva Anantharaman ; Paliath Narendran ; Michael Rusinowitch
Source-Tracking Unification / Venkatesh Choppella ; Christopher T. Haynes
Optimizing Higher-Order Pattern Unification / Brigitte Pientka ; Frank Pfenning
Decidability of Arity-Bounded Higher-Order Matching / Manfred Schmidt-Schauß
Author Index
Invited Talk / Session 1:
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking / Edmund M. Clarke
Session 2
5.

図書

図書
William McCune (ed.)
出版情報: Berlin ; New York : Springer, c1997  xiv, 462 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1249 . Lecture notes in artificial intelligence
所蔵情報: loading…
6.

図書

図書
M.A. McRobbie, J.K. Slaney, (eds.)
出版情報: Berlin ; New York : Springer, c1996  xv, 764 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1104 . Lecture notes in artificial intelligence
所蔵情報: loading…
7.

図書

図書
E. Lusk, R. Overbeek (eds.)
出版情報: Berlin ; Tokyo : Springer-Verlag, c1988  x, 775 p. ; 25 cm
シリーズ名: Lecture notes in computer science ; 310
所蔵情報: loading…
8.

図書

図書
edited by R.E. Shostak
出版情報: Berlin ; Tokyo : Springer-Verlag, 1984  vi, 508 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 170
所蔵情報: loading…
9.

図書

図書
Alan Bundy (ed.)
出版情報: Berlin ; Tokyo : Springer-Verlag, c1994  xvi, 848 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 814 . Lecture notes in artificial intelligence
所蔵情報: loading…
10.

図書

図書
M.E. Stickel (ed.)
出版情報: Berlin ; Tokyo : Springer-Verlag, c1990  xvi, 688 p. ; 25 cm
シリーズ名: Lecture notes in computer science ; 449 . Lecture notes in artificial intelligence
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼