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.

図書

図書
Peter J. Stuckey (ed.)
出版情報: Berlin : Springer, c2002  xi, 486 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2401
所蔵情報: loading…
3.

図書

図書
Uwe Egly, Christian G. Fermüller (eds.)
出版情報: Berlin : Springer, c2002  x, 339 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2381 . Lecture notes in artificial intelligence
所蔵情報: loading…
4.

図書

図書
Victor A. Carreño, César A. Muñoz, Sofiène Tahar (eds.)
出版情報: Berlin : Springer, c2002  x, 347 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2410
所蔵情報: loading…
目次情報: 続きを見る
Invited Talks
Formal Methods at NASA Langley / RickyButler
Higher Order Unification 30 Years Later / Gérard Huet
Regular Papers
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction / Simon J. Ambler ; RoyL. Crole ; Alberto Momigliano
Efficient Reasoning about Executable Specifications in Coq / Gilles Barthe ; Pierre Courtieu
Verified Bytecode Model Checkers / David Basin ; Stefan Friedrich ; Marek Gawkowski
The 5 Colour Theorem in Isabelle/Isar / Gertrud Bauer ; Tobias Nipkow
Type-Theoretic Functional Semantics / Yves Bertot ; Venanzio Capretta ; Kuntal Das Barman
A Proposal for a Formal OCL Semantics in Isabelle/HOL / Achim D. Brucker ; Burkhart Wolff
Explicit Universes for the Calculus of Constructions / Judicaël Courant
Formalised Cut Admissibility for Display Logic / JeremyE. Dawson ; Rajeev GorÆe
Formalizing the Trading Theorem for the Classification of Surfaces / Christophe Dehlinger ; Jean-Francois Dufourd
Free-Style Theorem Proving / David Delahaye
A Comparison of Two Proof Critics: Power vs. Robustness / Louise A. Dennis ; Alan Bundy
Two-Level Meta-reasoning in Coq / AmyP. Felty
PuzzleTool: An Example of Programming Computation and Deduction / Michael J.C. Gordon
A Formal Approach to Probabilistic Termination / Joe Hurd
Using Theorem Proving for Numerical Analysis / Micaela Mayero
Quotient Types: A Modular Approach / AlekseyNogin
Sequent Schema for Derived Rules / Jason Hickey
Algebraic Structures and Dependent Records / Virgile Prevosto ; Damien Doligez ; Therese Hardin
Proving the Equivalence of Microstep and Macrostep Semantics / Klaus Schneider
Weakest Precondition for General Recursive Programs Formalized in Coq / Xingyuan Zhang ; Malcolm Munro ; Mark Harman ; Lin Hu
Author Index
Invited Talks
Formal Methods at NASA Langley / RickyButler
Higher Order Unification 30 Years Later / Gérard Huet
5.

図書

図書
Reinhard Kahle, Peter Schroeder-Heister, Robert Stärk (eds.)
出版情報: Berlin ; Tokyo : Springer, c2001  viii, 238 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2183
所蔵情報: loading…
目次情報: 続きを見る
Linear Ramified Higher Type Recursion and Parallel Complexity / Klaus Aehlig ; Jan Johannsen ; Helmut Schwichtenberg ; Sebastiaan A. Terwijn
Reflective λ-Calculus / Jesse Alt ; Sergei Artemov
A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity / Matthias Baaz ; Christian G. Fermuller
Comparing the Complexity of Cut-Elimination Methods / Alexander Leitsch
Program Extraction from Gentzen's Proof of Transfinite Induction up to ε0 / Ulrich Berger
Coherent Bicartesian and Sesquicartesian Categories / Kosta DoÜen ; Zoran Petri?
Indexed Induction-Recursion / Peter Dybjer ; Anton Setzer
Modeling Meta-logical Features in a Calculus with Frozen Variables / Birgit Elbl
Proof Theory and Post-turing Analysis / Lew Gordeew
Interpolation for Natural Deduction with Generalized Eliminations / Ralph Matthes
Implicit Characterizations of Pspace / Isabel Oitavem
Iterate Logic / Peter H. Schmitt
Constructive Foundations for Featherweight Java / Thomas Studer
Author Index
Linear Ramified Higher Type Recursion and Parallel Complexity / Klaus Aehlig ; Jan Johannsen ; Helmut Schwichtenberg ; Sebastiaan A. Terwijn
Reflective λ-Calculus / Jesse Alt ; Sergei Artemov
A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity / Matthias Baaz ; Christian G. Fermuller
6.

図書

図書
Robert Nieuwenhuis, Andrei Voronkov (eds.)
出版情報: Berlin ; New York : Springer, c2001  xv, 738 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2250 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
Invited Talk / Session 1:
Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D / Ian Hodkinson ; Frank Wolter ; Michael Zakharyaschev
Verification / Session 2:
On Bounded Specifications / Orna Kupferman ; Moshe Y. Vardi
Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy / Klaus Schneider
Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets / Volker Diekert ; Paul Gastin
Guarded Logics / Session 3:
Games and Model Checking for Guarded Logics / Dietmar Berwanger ; Erich Grädel
Computational Space Efficiency and Minimal Model Generation for Guarded Formulae / Lilia Georgieva ; Ullrich Hustadt ; Renate A. Schmidt
Agents / Session 4:
Local Conditional High-Level Robot Programs / Natasha Alechina ; Brian Logan ; Sebastian SardiñaLogical Omniscience and the Cost of Deliberation:
A Refinement Theory That Supports Reasoning about Knowledge and Time for Synchronous Agents / Kai Engelhardt ; Ron van der Meyden ; Yoram Moses
Automated Theorem Proving / Session 5:
Proof and Model Generation with Disconnection Tableaux / Reinhold Letz ; Gernot Stenz
Counting the Number of Equivalent Binary Resolution Proofs / Joseph D. Horton
Splitting through New Proposition Symbols / Hans de NivelleSession 6:
Complexity of Linear Standard Theories / Christopher Lynch ; Barbara Morawska
Herbrand's Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving / Matthias Baaz ; Agata Ciabattoni ; Christian G. Fermüller
Non-classical Logics / Session 7:
Unification in a Description Logic with Transitive Closure of Roles / Franz Baader ; Ralf Küsters
Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions / Guy Perrier
Types / Session 8:
Coherence and Transitivity in Coercive Subtyping / Yong Luo ; Zhaohui Luo
A Type-Theoretic Approach to Induction with Higher-Order Encodings / Carsten Schürmann
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification / Jan-Georg Smaus
Experimental Papers / Session 9:
First-Order Atom Definitions Extended / Miyuki Koshimura ; Hiroshi Fujita ; Ryuzo Hasegawa ; Bijan Afshordel ; Thomas Hillenbrand ; Christoph WeidenbachModel Generation with Boolean Constraints:
Automated Proof Support for Interval Logics / Thomas Marthedal Rasmussen
Foundations of Logic / Session 10:
The Functions Provable by First Order Abstraction / Daniel Leivant
A Local System for Classical Logic / Kai Brunnler ; Alwen Fernanto Tiu
CSP and SAT / Session 11:
Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae / Jussi Rintanen
Permutation Problems and Channelling Constraints / Toby Walsh
Simplifying Binary Propositional Theories into Connected Components Twice as Fast / Alvaro del Val
Non-monotonic Reasoning / Session 12:
Reasoning about Evolving Nonmonotonic Knowledge Bases / Thomas Eiter ; Michael Fink ; Giuliana Sabbatini ; Hans Tompits
Efficient Computation of the Well-Founded Model Using Update Propagation / Andreas Behrend
Semantics / Session 13:
Indexed Categories and Bottom-Up Semantics of Logic Programs / Gianluca Amato ; James Lipton
Functional Logic Programming with Failure: A Set-Oriented View / F.J. Lopez-Fraguas ; J. Sanchez-Hernandez
Operational Semantics for Fixed-Point Logics on Constraint Databases / Stephan Kreutzer
Efficient Negation Using Abstract Interpretation / Susana Muñoz ; Juan José Moreno ; Manuel HermenegildoSession 14:
Certifying Synchrony for Free / Sylvain Boulmé ; Grégoire Hamon
A Computer Environment for Writing Ordinary Mathematical Proofs / David McMath ; Marianna Rozenfeld ; Richard Sommer
Termination / Session 15:
On Termination of Meta-programs / Alexander Serebrenik ; Danny De Schreye
A Monotonic Higher-Order Semantic Path Ordering / Cristina Borralleras ; Albert Rubio
Knowledge-Based Systems / Session 16:
The Elog Web Extraction Language / Robert Baumgartner ; Sergio Flesca ; Georg Gottlob
Census Data Repair: A Challenging Application of Disjunctive Logic Programming / Enrico Franconi ; Antonio Laureti Palma ; Nicola Leone ; Simona Perri ; Francesco Scarcello
Analysis of Logic Programs / Session 17:
Boolean Functions for Finite-Tree Dependencies / Roberto Bagnara ; Enea Zaffanella ; Roberta Gori ; Patricia M. Hill
How to Transform an Analyzer into a Verifier / Marco Comini ; Giorgio Levi
Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search / Rong Yang ; Steve Gregory
Databases and Knowledge Bases / Session 18:
Coherent Composition of Distributed Knowledge-Bases through Abduction / Ofer Arieli ; Bert Van Nuffelen ; Marc Denecker ; Maurice Bruynooghe
Tableaux for Reasoning about Atomic Updates / Georg Moser ; Richard Zach
Inference of Termination Conditions for Numerical Loops in Prolog / Session 19:
Termination of Rewriting with Strategy Annotations / Salvador Lucas
Inferring Termination Conditions for Logic Programs Using Backwards Analysis / Samir Genaim ; Michael Codish
Program Analysis and Proof Planning / Session 20:
Reachability Analysis of Term Rewriting Systems with Timbuk / Thomas Genet ; Valerie Viet Triem Tong
Binding-Time Annotations without Binding-Time Analysis / Wim Vanhoof
Concept Formation via Proof Planning Failure / Raúl Monroy
Author Index
Invited Talk / Session 1:
Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D / Ian Hodkinson ; Frank Wolter ; Michael Zakharyaschev
Verification / Session 2:
7.

図書

図書
Philippe Codognet (ed.)
出版情報: Berlin ; New York : Springer, c2001  xi, 364 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2237
所蔵情報: loading…
8.

図書

図書
Rajeev Goré, Alexander Leitsch, Tobias Nipkow (eds.)
出版情報: Berlin : Springer, c2001  xv, 708 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2083 . Lecture notes in artificial intelligence
所蔵情報: loading…
9.

図書

図書
Paul Callaghan ... [et al.] (eds.)
出版情報: Berlin ; New York : Springer, c2002  viii, 242 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2277
所蔵情報: loading…
目次情報: 続きを見る
Collection Principles in Dependent Type Theory / Peter Aczel ; Nicola Gambino
Executing Higher Order Logic / Stefan Berghofer ; Tobias Nipkow
ATour with Constructive Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio
An Implementation of Type: Type / Thierry Coquand ; Makoto Takeyama
On the Logical Content of Computational Type Theory: A Solution to CurryÆs Problem / Matt Fairtlough ; Michael Mendler
Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers ; Milad Niqui
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Freek Wiedijk ; Jan Zwanenburg
AKripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen
Towards Limit Computable Mathematics / Susumu Hayashi ; Masahiro Nakata
Formalizing the Halting Problem in a Constructive Type Theory / Kristofer Johannisson
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory / Giuseppe Longo
Changing Data Structures in Type Theory: AStudy of Natural Numbers / Nicolas Magaud ; Yves Bertot
Elimination with a Motive / Conor McBride
Generalization in Type Theory Based Proof Assistants / Olivier Pons
An Inductive Version of Nash-WilliamsÆ Minimal-Bad-Sequence Argument for HigmanÆs Lemma / Monika Seisenberger
Author Index
Collection Principles in Dependent Type Theory / Peter Aczel ; Nicola Gambino
Executing Higher Order Logic / Stefan Berghofer ; Tobias Nipkow
ATour with Constructive Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio
10.

図書

図書
Richard J. Boulton, Paul B. Jackson (eds.)
出版情報: Berlin : Springer, c2001  x, 393 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2152
所蔵情報: loading…
目次情報: 続きを見る
Invited Talks
JavaCard Program Verification / Bart Jacobs
View from the Fringe of the Fringe (Joint with CHARME 2001) / Steven D. Johnson
Using Decision Procedures with a Higher-Order Logic / Natarajan Shankar
Regular Contributions
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS / Andrew Adams ; Martin Dunstan ; Hanne Gottliebsen ; Tom Kelsey ; Ursula Martin ; Sam Owre
An Irrational Construction of R from Z / Rob D. Arthan
HELM and the Semantic Math-Web / Andrea Asperti ; Luca Padovani ; Claudio Sacerdoti Coen ; Irene Schena
Calculational Reasoning Revisited (An Isabelle/Isar Experience) / Gertrud Bauer ; Markus Wenzel
Mechanical Proofs about a Non-repudiation Protocol / Giampaolo Bella ; Lawrence C. Paulson
Proving Hybrid Protocols Correct / Mark Bickford ; Christoph Kreitz ; Robbert van Renesse ; Xiaoming Liu
Nested General Recursion and Partiality in Type Theory / Ana Bove ; Venanzio Capretta
A Higher-Order Calculus for Categories / Mario Cáccamo ; Glynn Winskel
Certifying the Fast Fourier Transform with Coq
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing / Marc Daumas ; Laurence Rideau ; Laurent Théry
Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain / Louise A. Dennis ; Alan Smaill
Abstraction and Refinement in Higher Order Logic / Matt Fairtlough ; Michael Mendler ; Xiaochun Cheng
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL / Simon J. Gay
Representing Hierarchical Automata in Interactive Theorem Provers / Steffen Helke ; Florian Kammüller
Refinement Calculus for Logic Programming in Isabelle/HOL / David Hemer ; Ian Hayes ; Paul Strooper
Predicate Subtyping with Predicate Sets / Joe Hurd
A Structural Embedding of Ocsid in PVS / Pertti Kellomaki
A Certified Polynomial-Based Decision Procedure for Propositional Logic / Inmaculada Medina-Bulo ; Francisco Palomo-Lozano ; José A. Alonso-Jiménez
Finite Set Theory in ACL2 / J Strother Moore
The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability) / Pavel Naumov ; Mark-Oliver Stehr ; José Meseguer
Formalizing Convex Hull Algorithms / David Pichardie ; Yves Bertot
Experiments with Finite Tree Automata in Coq / Xavier Rival ; Jean Goubault-Larrecq
Mizar Light for HOL Light / Freek Wiedijk
Author Index
Invited Talks
JavaCard Program Verification / Bart Jacobs
View from the Fringe of the Fringe (Joint with CHARME 2001) / Steven D. Johnson
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼