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.

図書

図書
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
3.

図書

図書
Jürgen Richter-Gebert, Dongming Wang (eds.)
出版情報: Berlin : Springer, c2001  viii, 323 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2061 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
On Spatial Constraint Solving Approaches / Christoph M. Hoffmann ; Bo Yuan
A Hybrid Method for Solving Geometric Constraint Problems / Xiao-Shan Gao ; Lei-Dong Huang ; Kun Jiang
Solving the Birkhoff Interpolation Problem via the Critical Point Method: An Experimental Study / Fabrice Rouillier ; Mohab Safey El Din ; Éric Schost
A Practical Program of Automated Proving for a Class of Geometric Inequalities / Lu Yang ; Ju Zhang
Randomized Zero Testing of Radical Expressions and Elementary Geometry Theorem Proving / Daniela Tulone ; Chee Yap ; Chen Li
Algebraic and Semialgebraic Proofs: Methods and Paradoxes / Pasqualina Conti ; Carlo Traverso
Remarks on Geometric Theorem Proving / Laura Bazzotti ; Giorgio Dalzotto ; Lorenzo Robbiano
The Kinds of Truth of Geometry Theorems / Michael Bulmer ; Desmond Fearnley-Sander ; Tim Stokes
A Complex Change of Variables for Geometrical Reasoning
Reasoning about Surfaces Using Differential Zero and Ideal Decomposition / Philippe Aubry ; Dongming Wang
Effective Methods in Computational Synthetic Geometry / Jürgen Bokowski
Decision Complexity in Dynamic Geometry / Ulrich Kortenkamp ; Jürgen Richter-Gebert
Automated Theorem Proving in Incidence Geometry - A Bracket Algebra Based Elimination Method / Hongbo Li ; Yihong Wu
Qubit Logic, Algebra and Geometry / Timothy F. Havel
Nonstandard Geometric Proofs / Jacques D. Fleuriot
Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization / Ricardo Caferra ; Nicolas Peltier ; François Puitg
Higher-Order Intuitionistic Formalization and Proofs in HilbertÆs Elementary Geometry / Christophe Dehlinger ; Jean-François Dufourd ; Pascal Schreck
Author Index
On Spatial Constraint Solving Approaches / Christoph M. Hoffmann ; Bo Yuan
A Hybrid Method for Solving Geometric Constraint Problems / Xiao-Shan Gao ; Lei-Dong Huang ; Kun Jiang
Solving the Birkhoff Interpolation Problem via the Critical Point Method: An Experimental Study / Fabrice Rouillier ; Mohab Safey El Din ; Éric Schost
4.

図書

図書
Hoon Hong, Dongming Wang (eds.)
出版情報: Berlin : Springer, c2006  x, 211 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3763 . Lecture notes in artificial intelligence
所蔵情報: loading…
5.

図書

図書
Xiao-Shan Gao, Dongming Wang, Lu Yang (eds.)
出版情報: Berlin : Springer, c1999  vi, 285 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1669 . Lecture notes in artificial intelligence
所蔵情報: loading…
目次情報: 続きを見る
Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving / Wen-tsün Wu
Solving Geometric Problems with Real Quantifier Elimination / Andreas Dolzmann
Automated Discovering and Proving for Geometric Inequalities / Lu Yang ; Xiaorong Hou ; Bican Xia
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle / Jacques D. Fleuriot ; Lawrence C. Paulson
Readable Machine Solving in Geometry and ICAI Software MSG / Chuan-Zhong Li ; Jing-Zhong Zhang
Plane Euclidean Reasoning / Desmond Fearnley-Sander
A Clifford Algebraic Method for Geometric Reasoning / Haiquan Yang ; Shugong Zhang ; Guochen Feng
Clifford Term Rewriting for Geometric Reasoning in 3D / Thierry Boy de la Tour ; Stéphane Fèvre ; Dongming Wang
Some Applications of Clifford Algebra to Geometries / Hongbo Li
Decomposing Algebraic Varieties
An Application of Automatic Theorem Proving in Computer Vision / Didier Bondyfalat ; Bernard Mourrain ; Thèodore Papadopoulo
Automated Geometry Diagram Construction and Engineering Geometry / Xiao-Shan Gao
A 2D Geometric Constraint Solver for Parametric Design Using Graph Analysis and Reduction / Jae Yeol Lee
Variant Geometry Analysis and Synthesis in Mechanical CAD / Zongying Ou ; Jun Liu
Author Index
Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving / Wen-tsün Wu
Solving Geometric Problems with Real Quantifier Elimination / Andreas Dolzmann
Automated Discovering and Proving for Geometric Inequalities / Lu Yang ; Xiaorong Hou ; Bican Xia
6.

図書

図書
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…
7.

図書

図書
Jim Grundy, Malcolm Newey (eds.)
出版情報: Berlin ; Tokyo : Springer, c1998  viii, 496 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1479
所蔵情報: loading…
目次情報: 続きを見る
Invited Papers
Verified Lexical Analysis / Tobias Nipkow
Extending Window Inference / Joakim von Wright
Refereed Papers
Program Abstraction in a Higher-Order Logic Framework / Marco Benini ; Sara Kalvala ; Dirk Nowotka
The Village Telephone System: A Case Study in Formal Software Engineering / Karthikeyan Bhargavan ; Carl A. Gunter ; Elsa L. Gunter ; Michael Jackson ; Davor Obradovic ; Pamela Zave
Generating Embeddings from Denotational Descriptions / Richard J. Boulton
An Interface between CLaM and HOL / Richard Boulton ; Konrad Slind ; Alan Bundy ; Mike Gordon
Classical Propositional Decidability via Nuprl Proof Extraction / James L. Caldwell
A Comparison of PVS and Isabelle/HOL / David Griffioen ; Marieke Huisman
Adding External Decision Procedures to HOL90 Securely
Formalizing Basic First Order Model Theory / John Harrison
Formalizing Dijkstra
Mechanical Verification of Total Correctness through
Diversion Verification Conditions / Peter V. Homeier ; David F. Martin
A Type Annotation Scheme for Nuprl / Douglas J. Howe
Verifying a Garbage Collection Algorithm / Paul B. Jackson
Hot: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux / Karsten Konrad
Free Variables and Subexpressions in Higher-Order Meta Logic / Chuck Liang
An LPO-Based Termination Ordering for Higher-Order Terms without ?-Abstraction / Maxim Lifantsev ; Leo Bachmair
Proving Isomorphism of First-Order Logic Proof Systems in HOL / Anna Mikhajlova
Exploiting Parallelism in Interactive Theorem Provers / Roderick Moten
I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle / Olaf Müller
Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic / Wolfgang Naraschewski ; Markus Wenzel
On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System / Naren Narasimhan ; Ranga Vemuri
Co-inductive Axiomatization of a Synchronous Language / David Nowak ; Jean-Rene Beauvais ; Jean-Pierre Talpin
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling / François Puitg ; Jean-François Dufourd
A Tool for Data Refinement / Rimvydas RukÃœenas
Mechanizing Relevant Logics with HOL / Hajime Sawamura ; Daisaku Asanuma
Case Studies in Meta-Level Theorem Proving / Friedrich W. von Henke ; Stephan Pfab ; Holger Pfeifer ; Harald Rueß
Formalization of Graph Search Algorithms and Its Applications / Mitsuharu Yamamoto ; Koichi Takahashi ; Masami Hagiya ; Shin-ya Nishizaki ; Tetsuo Tamai
Author Index
Invited Papers
Verified Lexical Analysis / Tobias Nipkow
Extending Window Inference / Joakim von Wright
8.

図書

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

図書

図書
Yves Bertot ... [et al.] (eds.)
出版情報: Berlin : Springer, c1999  viii, 358 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1690
所蔵情報: loading…
10.

図書

図書
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
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼