default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID1st IJCAR 2001: Siena, Italy
- Rajeev Goré, Alexander Leitsch, Tobias Nipkow:
Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings. Lecture Notes in Computer Science 2083, Springer 2001, ISBN 3-540-42254-4
Invited Talks
- Neil D. Jones:
Program Termination Analysis by Size-Change Graphs (Abstract). 1-4 - Lawrence C. Paulson:
SET Cardholder Registration: The Secrecy Proofs. 5-12 - Andrei Voronkov:
Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. 13-28
Description, Modal and Temporal Logics
- Volker Haarslev, Ralf Möller, Michael Wessel:
The Description Logic ALCNHR+ Extended with Concrete Domains: A Practically Motivated Approach. 29-44 - Carsten Lutz:
NEXPTIME-Complete Description Logics with Concrete Domains. 45-60 - Volker Haarslev, Ralf Möller, Anni-Yasmin Turhan:
Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics. 61-75 - Ulrike Sattler, Moshe Y. Vardi:
The Hybrid µ-Calculus. 76-91 - Franz Baader, Stephan Tobies:
The Inverse Method Implements the Automata Approach for Modal Satisfiability. 92-106 - Regimantas Pliuskevicius:
Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL. 107-120 - Carsten Lutz, Holger Sturm, Frank Wolter
, Michael Zakharyaschev:
Tableaux for Temporal Description Logic with Constant Domains. 121-136 - Serenella Cerrito, Marta Cialdea Mayer:
Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation. 137-151
Saturation Based Theorem Proving, Applications, and Data Structures
- Andrea Formisano, Eugenio G. Omodeo, Marco Temperini:
Instructing Equational Set-Reasoning with Otter. 152-167 - Stefan Szeider:
NP-Completeness of Refutability by Literal-Once Resolution. 168-181 - Reiner Hähnle, Neil V. Murray, Erik Rosenthal:
Ordered Resolution vs. Connection Graph Resolution. 182-194 - Jürgen Stuber:
A Model-Based Completeness Proof of Extended Narrowing and Resolution. 195-210 - Hans de Nivelle, Ian Pratt-Hartmann:
A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality. 211-225 - Uwe Waldmann:
Superposition and Chaining for Totally Ordered Divisible Abelian Groups. 226-241 - Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela:
Context Trees. 242-256 - Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov:
On the Evaluation of Indexing Techniques for Theorem Proving. 257-271
Logic Programming and Nonmonotonic Reasoning
- Sylvie Doutre, Jérôme Mengin:
Preferred Extensions of Argumentation Frameworks: Query Answering and Computation. 272-288 - Pablo A. Armelín, David J. Pym:
Bunched Logic Programming. 289-304 - Kewen Wang:
A Top-Down Procedure for Disjunctive Well-Founded Semantics. 305-317 - Michael Beeson:
A Second-Order Theorem Prover Applied to Circumscription. 318-324 - Christian Anger, Kathrin Konczak, Thomas Linke:
NoMoRe : A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semantics. 325-330
Propositional Satisfiability and Quantified Boolean Logic
- Marco Benedetti:
Conditional Pure Literal Graphs. 331-346 - Enrico Giunchiglia, Marco Maratea, Armando Tacchella, Davide Zambonin:
Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability. 347-363 - Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella:
QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. 364-369 - Stephan Schulz:
System Abstract: E 0.61. 370-375 - Alexandre Riazanov, Andrei Voronkov:
Vampire 1.1 (System Description). 376-380 - Reinhold Letz, Gernot Stenz:
DCTP - A Disconnection Calculus Theorem Prover - System Abstract. 381-385
Logical Frameworks, Higher-Order Logic, Interactive Theorem Proving
- Marko Luther:
More On Implicit Syntax. 386-400 - Brigitte Pientka:
Termination and Reduction Checking for Higher-Order Logic Programs. 401-415 - Armin Fiedler:
P.rex: An Interactive Proof Explainer. 416-420 - Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin:
JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. 421-426
Semantic Guidance
- Gilles Audemard, Laurent Henocque:
The eXtended Least Number Heuristic. 427-442 - Kahlil Hodgson, John K. Slaney:
System Description: SCOTT-5. 443-447 - Maria Paola Bonacina:
Combination of Distributed Search and Multi-search in Peers-mcd.d. 448-452 - Luis Fariñas del Cerro, David Fauthoux, Olivier Gasquet, Andreas Herzig, Dominique Longin, Fabio Massacci:
Lotrec : The Generic Tableau Prover for Modal and Description Logics. 453-458 - Jens Happe:
The MODPROF Theorem Prover. 459-463 - Peter F. Patel-Schneider, Roberto Sebastiani:
A New System and Methodology for Generating Random Modal Formulae. 464-468
Equational Theorem Proving and Term Rewriting
- Jürgen Giesl, Deepak Kapur:
Decidable Classes of Inductive Theorems. 469-484 - Xavier Urbain:
Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems. 485-498 - Christopher Lynch, Barbara Morawska:
Decidability and Complexity of Finitely Closable Linear Equational Theories. 499-513 - Harald Ganzinger, David A. McAllester:
A New Meta-complexity Theorem for Bottom-Up Logic Programs. 514-528
Tableau, Sequent, Natural Deduction Calculi and Proof Theory
- Arnon Avron, Iddo Lev:
Canonical Propositional Gentzen-Type Systems. 529-544 - Martin Giese:
Incremental Closure of Free Variable Tableaux. 545-560 - Uwe Egly, Stephan Schmitt:
Deriving Modular Programs from Short Proofs. 561-577 - Nicolas Peltier:
A General Method for Using Schematizations in Automated Deduction. 578-592
Automata, Specification, Verification, and Logics of Programs
- Aart Middeldorp:
Approximating Dependency Graphs Using Tree Automata Techniques. 593-610 - Bernard Boigelot, Sébastien Jodogne, Pierre Wolper:
On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. 611-625 - Bernhard Beckert, Steffen Schlager:
A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities. 626-641 - Wolfgang Reif, Gerhard Schellhorn, Andreas Thums:
Flaw Detection in Formal Specifications. 642-657 - Jürgen Avenhaus, Bernd Löchner:
CCE: Testing Ground Joinability. 658-662 - Alessandro Armando, Luca Compagna, Silvio Ranise:
System Description: RDL : Rewrite and Decision Procedure Laboratory. 663-669 - Joshua S. Hodas, Naoyuki Tamura:
lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic. 670-684
Nonclassical Logics
- Dominique Pastre:
MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction. 685-689 - Jörg Lücke:
Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory. 690-695 - Dominique Larchey-Wendling, Daniel Méry, Didier Galmiche:
STRIP: Structural Sharing for Efficient Proof-Search. 696-700 - Volker Haarslev, Ralf Möller:
RACER System Description. 701-706
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 2025-11-16 00:24 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:
