zbMATH — the first resource for mathematics

Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. (English) Zbl 0968.00052
Lecture Notes in Computer Science 2083. Lecture Notes in Artificial Intelligence. Berlin: Springer. xv, 708 p. (2001).

Show indexed articles as search result.

The articles of this volume will be reviewed individually.
Indexed articles:
Jones, Neil D., Program termination analysis by size-change graphs (abstract), 1-4 [Zbl 0988.68732]
Paulson, Lawrence C., SET cardholder registration: The secrecy proofs (extended abstract), 5-12 [Zbl 0988.68739]
Voronkov, Andrei, Algorithms, datastructures, and other issues in efficient automated deduction, 13-28 [Zbl 0988.68585]
Haarslev, Volker; Möller, Ralf; Wessel, Michael, The description logic \(\mathcal{ALCNH}_{R+}\) extended with concrete domains: A practically motivated approach, 29-44 [Zbl 0988.68182]
Lutz, Carsten, NEXPTIME-complete description logics with concrete domains, 45-60 [Zbl 0988.68175]
Haarslev, Volker; Möller, Ralf; Turhan, Anni-Yasmin, Exploiting pseudo models for TBox and ABox reasoning in expressive description logics, 61-75 [Zbl 0988.68181]
Sattler, Ulrike; Vardi, Moshe Y., The hybrid \(\mu\)-calculus, 76-91 [Zbl 0988.03053]
Baader, Franz; Tobies, Stephan, The inverse method implements the automata approach for modal satisfiability, 92-106 [Zbl 0988.03021]
Pliuškevičius, Regimantas, Deduction-based decision procedure for a clausal miniscoped fragment of FTL, 107-120 [Zbl 0988.03018]
Lutz, Carsten; Sturm, Holger; Wolter, Frank; Zakharyaschev, Michael, Tableaux for temporal description logic with constant domains, 121-136 [Zbl 0988.68178]
Cerrito, Serenella; Cialdea Mayer, Marta, Free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation, 137-151 [Zbl 0988.03032]
Formisano, Andrea; Omodeo, Eugenio G.; Temperini, Marco, Instructing equational set-reasoning with Otter, 152-167 [Zbl 0988.68164]
Szeider, Stefan, NP-completeness of refutability by literal-once resolution, 168-181 [Zbl 0988.03020]
Hähnle, Reiner; Murray, Neil V.; Rosenthal, Erik, Ordered resolution vs. connection graph resolution, 182-194 [Zbl 0990.68539]
Stuber, Jürgen, A model-based completeness proof of extended narrowing and resolution, 195-210 [Zbl 0988.03016]
de Nivelle, Hans; Pratt-Hartmann, Ian, A resolution-based decision procedure for the two-variable fragment with equality, 211-225 [Zbl 0988.03023]
Waldmann, Uwe, Superposition and chaining for totally ordered divisible abelian groups (extended abstract), 226-241 [Zbl 0988.03510]
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar, Context trees, 242-256 [Zbl 0988.68588]
Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei, On the evaluation of indexing techniques for theorem proving, 257-271 [Zbl 0988.68595]
Doutre, Sylvie; Mengin, Jérôme, Preferred extensions of argumentation frameworks: Query, answering, and computation, 272-288 [Zbl 0990.68541]
Armelín, Pablo A.; Pym, David J., Bunched logic programming (extended abstract), 289-304 [Zbl 0988.68508]
Wang, Kewen, A top-down procedure for disjunctive well-founded semantics, 305-317 [Zbl 0988.68032]
Beeson, Michael, A second-order theorem prover applied to circumscription, 318-324 [Zbl 0988.68583]
Anger, Christian; Konczak, Kathrin; Linke, Thomas, NoMoRe: A system for non-monotonic reasoning with logic programs under answer set semantics, 325-330 [Zbl 0988.68518]
Benedetti, Marco, Conditional pure literal graphs, 331-346 [Zbl 0990.68131]
Giunchiglia, Enrico; Maratea, Massimo; Tacchella, Armando; Zambonin, Davide, Evaluating search heuristics and optimization techniques in propositional satisfiability, 347-363 [Zbl 0988.68608]
Giunchiglia, Enrico; Narizzano, Massimo; Tacchella, Armando, QUBE: A system for deciding quantified Boolean formulas satisfiability, 364-369 [Zbl 0988.68598]
Schulz, Stephan, System abstract: E 0. 61, 370-375 [Zbl 0988.68602]
Riazanov, Alexandre; Voronkov, Andrei, Vampire 1. 1 (system description), 376-380 [Zbl 0988.68607]
Letz, Reinhold; Stenz, Gernot, DCTP – a disconnection calculus theorem prover – system abstract, 381-385 [Zbl 0988.68589]
Luther, Marko, More on implicit syntax, 386-400 [Zbl 0988.68593]
Pientka, Brigitte, Termination and reduction checking for higher-order logic programs, 401-415 [Zbl 0988.68514]
Fiedler, Armin, P. rex: An interactive proof explainer, 416-420 [Zbl 0988.68596]
Schmitt, Stephan; Lorigo, Lori; Kreitz, Christoph; Nogin, Aleksey, JProver: Integrating connection-based theorem proving into interactive proof assistants, 421-426 [Zbl 0988.68609]
Audemard, Gilles; Henocque, Laurent, The eXtended least number heuristic, 427-442 [Zbl 0988.68605]
Hodgson, Kahlil; Slaney, John, System description: SCOTT-5, 443-447 [Zbl 0988.68603]
Bonacina, Maria Paola, Combination of distributed search and multi-search in peers-mcd. d. (system description), 448-452 [Zbl 0988.68611]
Fariñas del Cerro, Luis; Fauthoux, David; Gasquet, Olivier; Herzig, Andreas; Longin, Dominique, Lotrec: The generic tableau prover for modal and description logics, 453-458 [Zbl 0988.68592]
Happe, Jens, The MODPROF theorem prover, 459-463 [Zbl 0988.68606]
Patel-Schneider, Peter F.; Sebastiani, Roberto, A new system and methodology for generating random modal formulae, 464-468 [Zbl 0988.68582]
Giesl, Jürgen; Kapur, Deepak, Decidable classes of inductive theorems, 469-484 [Zbl 0988.03017]
Urbain, Xavier, Automated incremental termination proofs for hierarchically defined term rewriting systems, 485-498 [Zbl 0988.68094]
Lynch, Christopher; Morawska, Barbara, Decidability and complexity of finitely closable linear equational theories, 499-513 [Zbl 0988.03013]
Ganzinger, Harald; McAllester, David, A new meta-complexity theorem for bottom-up logic programs, 514-528 [Zbl 0988.68031]
Avron, Arnon; Lev, Iddo, Canonical propositional Gentzen-type systems, 529-544 [Zbl 0988.03011]
Giese, Martin, Incremental closure of free variable tableaux, 545-560 [Zbl 0988.03019]
Egly, Uwe; Schmitt, Stephan, Deriving modular programs from short proofs, 561-577 [Zbl 0988.03086]
Peltier, Nicolas, A general method for using schematizations in automated deduction, 578-592 [Zbl 0988.03015]
Middeldorp, Aart, Approximating dependency graphs using tree automata techniques, 593-610 [Zbl 0988.68162]
Boigelot, Bernard; Jodogne, Sébastien; Wolper, Pierre, On the use of weak automata for deciding linear arithmetic with integer and real variables, 611-625 [Zbl 0988.03022]
Beckert, Bernhard; Schlager, Steffen, A sequent calculus for first-order dynamic logic with trace modalities, 626-641 [Zbl 0988.03051]
Reif, Wolfgang; Schellhorn, G.; Thums, Andreas, Flaw detection in formal specifications, 642-657 [Zbl 0988.68107]
Avenhaus, Jürgen; Löchner, Bernd, CCE: Testing ground joinability, 658-662 [Zbl 0988.68587]
Armando, Alessandro; Compagna, Luca; Ranise, Silvio, System description: RDL: Rewrite and Decision procedure Laboratory, 663-669 [Zbl 0988.68557]
Hodas, Joshua S.; Tamura, Naoyuki, lolliCoP – a linear logic implementation of a lean connection-method theorem prover for first-order classical logic, 670-684 [Zbl 0988.68610]
Pastre, Dominique, MUSCADET 2. 3: A knowledge-based theorem prover based on natural deduction, 685-689 [Zbl 0988.68594]
Lücke, Jörg, Hilberticus – a tool deciding an elementary sublanguage of set theory, 690-695 [Zbl 0988.68591]
Larchey-Wendling, D.; Méry, D.; Galmiche, Didier, STRIP: Structural sharing for efficient proof-search, 696-700 [Zbl 0990.68540]
Haarslev, Volker; Möller, Ralf, RACER system description, 701-705 [Zbl 0988.68599]

00B25 Proceedings of conferences of miscellaneous specific interest
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
Full Text: DOI