close
1.

図書
図書
1. 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980 (: gw ; : us)
edited by W. Bibel and R. Kowalski
出版情報: Berlin ; New York : Springer-Verlag, 1980  vii, 385 p. ; 25 cm
シリーズ名: Lecture notes in computer science ; 87
所蔵情報: loading…
2.

図書
図書
2. 7th International Conference on Automated Deduction : Napa, California, USA, May 14-16, 1984 : proceedings (: gw ; : us)
edited by R.E. Shostak
出版情報: Berlin ; Tokyo : Springer-Verlag, 1984  vi, 508 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 170
所蔵情報: loading…
3.

図書
図書
3. 9th International Conference on Automated Deduction : Argonne, Illinois, USA, May 23-26, 1988 : proceedings (: gw ; : us)
E. Lusk, R. Overbeek (eds.)
出版情報: Berlin ; Tokyo : Springer-Verlag, c1988  x, 775 p. ; 25 cm
シリーズ名: Lecture notes in computer science ; 310
所蔵情報: loading…
4.

図書
図書
4. 6th Conference on Automated Deduction, New York, USA, June 7-9, 1982 (: gw ; : us)
edited by D.W. Loveland
出版情報: Berlin ; New York : Springer-Verlag, 1982  vii, 389 p. ; 25 cm
シリーズ名: Lecture notes in computer science ; 138
所蔵情報: loading…
5.

図書
図書
5. Theorem proving in higher order logics : 12th International Conference, TPHOLs '99, Nice, France, September 14-17, 1999 : proceedings
Yves Bertot ... [et al.] (eds.)
出版情報: Berlin : Springer, c1999  viii, 358 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1690
所蔵情報: loading…
6.

図書
図書
6. Automated deduction in geometry : Second International Workshop, ADG '98, Beijing, China, August 1-3, 1998 : proceedings
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
7.

図書
図書
7. Automated deduction - CADE-17 : 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000 : proceedings
David McAllester (ed.)
出版情報: Berlin : Springer, c2000  xiii, 512 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1831 . Lecture notes in artificial intelligence
所蔵情報: loading…
8.

図書
図書
8. Automated deduction in geometry : International Workshop on Automated Deduction in Geometry, Toulouse, France, September 27-29, 1996, selected papers
Dongming Wang (ed.)
出版情報: Berlin ; New York : Springer, c1997  234 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1360 . Lecture notes in artificial intelligence
所蔵情報: loading…
9.

図書
図書
9. Computational logic and proof theory : 5th Kurt Gödel Colloquim, KGC '97, Vienna, Austria, August 25-29, 1997 : proceedings (: pbk)
Georg Gottlob, Alexander Leitsch, Daniele Mundici, (eds.)
出版情報: Berlin ; Tokyo : Springer, c1997  viii, 348 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1289
所蔵情報: loading…
10.

図書
図書
10. Automated deduction - CADE-15 : 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998 : proceedings (: pbk)
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…
11.

図書
図書
11. Theorem proving in higher order logics : 11th International Conference, TPHOLs '98, Canberra, Australia, September 27- October 1, 1998 : proceedings
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
12.

図書
図書
12. Automated deduction, CADE-14 : 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997 : proceedings
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…
13.

図書
図書
13. Principles of data mining and knowledge discovery : First European Symposium, PKDD '97, Trondheim, Norway, June 24-27, 1997 : proceedings
Jan Komorowski, Jan Zytkow (eds.)
出版情報: Berlin ; Tokyo : Springer, c1997  ix, 396 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1263 . Lecture notes in artificial intelligence
所蔵情報: loading…
14.

図書
図書
14. Automated deduction -- CADE-13 : 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30-August 3, 1996 : proceedings
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…
15.

図書
図書
15. Automated deduction, CADE-11 : 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992 : proceedings (: gw ; : us)
D. Kapur (ed.)
出版情報: Berlin ; Tokyo : Springer-Verlag, c1992  xv, 793 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 607 . Lecture notes in artificial intelligence
所蔵情報: loading…
16.

図書
図書
16. Higher order logic theorem proving and its applications : proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications--HOL '92
organized by CHEOPS ESPRIT BRA 3215 ; sponsored by IMEC and the Commission of the European Communities, Leuven, Belgium, 21-24 September 1992 ; edited by Luc J.M. Claesen, Michael J.C. Gordon
出版情報: Amsterdam ; New York : North-Holland, 1993  xiii, 568 p. ; 23 cm
シリーズ名: IFIP transactions ; A . Computer science and technology ; 20
所蔵情報: loading…
17.

図書
図書
17. 10th International Conference on Automated Deduction : Kaiserslautern, FRG, July 24-27, 1990, proceedings (: gw ; : us)
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…
18.

図書
図書
18. Computational logic and proof theory : Third Kurt Gödel Colloquium, KGC '93, Brno, Czech Republic, August 24-27, 1993 : proceedings (: us ; : gw)
Georg Gottlob, Alexander Leitsch, Daniele Mundici, (eds.)
出版情報: Berlin ; New York : Springer-Verlag, c1993  xi, 348 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 713
所蔵情報: loading…
19.

図書
図書
19. Automated deduction, CADE-12 : 12th International Conference on Automated Deduction, Nancy, France, June 26-July 1, 1994 : proceedings (: us ; : gw)
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…
20.

図書
図書
20. Automated deduction - CADE-19 : 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28-August 2, 2003 : proceedings
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
21.

図書
図書
21. Automated deduction in geometry : 4th International Workshop, ADG 2002, Hagenberg Castle, Austria, September 4-6, 2002 : revised papers
Franz Winkler (ed.)
出版情報: Berlin ; Tokyo : Springer, c2004  vi, 229 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2930 . Lecture notes in artificial intelligence
所蔵情報: loading…
22.

図書
図書
22. Automated deduction -- CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings
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
23.

図書
図書
23. Automated deduction in geometry : 5th International Workshop, ADG 2004, Gainesville, FL, USA, September 16-18, 2004 : revised papers
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…
24.

図書
図書
24. Automated deduction in geometry : Third International Workshop, ADG 2000, Zurich, Switzerland, September 25-27, 2000 : revised papers
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
25.

図書
図書
25. Proof theory in computer science : international seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001 : proceedings
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
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼