default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID18th CADE 2002: Copenhagen, Denmark
- Andrei Voronkov:
Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings. Lecture Notes in Computer Science 2392, Springer 2002, ISBN 3-540-43931-5
Description Logics and Semantic Web
- Ian Horrocks:
Reasoning with Expressive Description Logics: Theory and Practice. 1-15 - Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi:
BDD-Based Decision Procedures for K. 16-30
Proof-Carrying Code and Compiler Verification
- Andrew Bernard, Peter Lee:
Temporal Logic for Proof-Carrying Code. 31-46 - Robert R. Schneck, George C. Necula:
A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code. 47-62 - Martin Strecker:
Formal Verification of a Java Compiler in Isabelle. 63-77
Non-classical Logics
- Uwe Egly:
Embedding Lax Logic into Intuitionistic Logic. 78-93 - Dominique Larchey-Wendling:
Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic. 94-110 - Didier Galmiche, Daniel Méry:
Connection-Based Proof Search in Propositional BI Logic. 111-128
System Descriptions
- Jesper B. Møller:
DDDLIB: A Library for Solving Quantified Difference Inequalities. 129-133 - Joe Hurd:
An LCF-Style Interface between HOL and First-Order Logic. 134-138 - Jürgen Zimmer, Michael Kohlhase:
System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning. 139-143 - Jörg H. Siekmann, Christoph Benzmüller, 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, Jürgen Zimmer:
Proof Development with OMEGA. 144-149 - Mateja Jamnik
, Manfred Kerber, Martin Pollet:
Learn Omega-matic: System Description. 150-155 - Carlos Areces, Juan Heguiabehere:
HyLoRes 1.0: Direct Resolution for Hybrid Logics. 156-160
SAT
- Eugene Goldberg:
Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. 161-180 - Thierry Boy de la Tour:
A Note on Symmetry Heuristics in SEM. 181-194 - Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani:
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. 195-210
Model Generation
- Wolfgang Ahrendt:
Deductive Search for Errors in Free Data Type Specifications Using Model Generation. 211-225 - Gilles Audemard, Belaid Benhamou:
Reasoning by Symmetry and Function Ordering in Finite Model Generation. 226-240 - Bernhard Gramlich, Reinhard Pichler:
Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations. 241-259 - Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt:
A New Clausal Class Decidable by Hyperresolution. 260-274
CASC
- Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobalt, Dalibor Topic:
S PASS Version 2.0. 275-279 - Stephan Schulz, Geoff Sutcliffe:
System Description: GrAnDe 1.0. 280-284 - Simon Colton:
The HR Program for Theorem Generation. 285-289 - Michael W. Whalen, Johann Schumann, Bernd Fischer:
AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description. 290-294
CADE-CAV Invited Talk
- Lintao Zhang, Sharad Malik:
The Quest for Efficient Boolean Satisfiability Solvers. 295-313 - Cristina Borralleras, Salvador Lucas, Albert Rubio:
Recursive Path Orderings Can Be Context-Sensitive. 314-331
Combination of Decision Procedures
- Harald Ganzinger:
Shostak Light. 332-346 - Jonathan Ford, Natarajan Shankar:
Formal Verification of a Combination Decision Procedure. 347-362 - Calogero G. Zarba:
Combining Multisets with Integers. 363-376
Logical Frameworks
- Lawrence C. Paulson:
The Reflection Theorem: A Study in Meta-theoretic Reasoning. 377-391 - Aaron Stump, David L. Dill:
Faster Proof Checking in the Edinburgh Logical Framework. 392-407 - Chad E. Brown:
Solving for Set Variables in Higher-Order Theorem Proving. 408-422
Model Checking
- Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi:
The Complexity of the Graded µ-Calculus. 423-437 - Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea:
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. 438-455
Equational Reasoning
- Miquel Bofill, Albert Rubio:
Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. 456-470 - Christopher Lynch, Barbara Morawska:
Basic Syntactic Mutation. 471-485 - Thomas Hillenbrand, Bernd Löchner:
The Next W ALDMEISTER Loop. 486-500
Proof Theory
- Jean-Marc Andreoli:
Focussing Proof-Net Construction as a Middleware Paradigm. 501-516 - Matthias Baaz:
Proof Analysis by Resolution. 517-532
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-21 20:37 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
